perf(Algebra/EuclideanDomain/Defs): prio decrease of EuclideanDomain.toCommRing

[kbuzzard]

This instance always applies, and is unlikely to be the right answer in practice.

---

[github-actions]

PR summary 7a3d8788df

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for cb31b2b against 7a3d878 are in. There are significant results. @kbuzzard

• ✅ build//instructions: -547.5G (-0.32%)

Large changes (1✅)

• ✅ build/module/Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple//instructions: -18.9G (-7.36%)

Medium changes (39✅)

Too many entries to display here. View the full report on radar instead.

Small changes (96✅)

Too many entries to display here. View the full report on radar instead.

[YaelDillies]

When doing this sort of change to attributes, priorities, etc... for non-trivial reasons, could you please leave comments in the code explaining what that reason is? eg here the priority reduction should get a comment saying "We want this to have lower priority than CommRing.toRing", and it would be perfect if you also added the properly dualised comment near CommRing.toRing.

This is important so that people don't acciden or intentionally undo it (although in this specific case a bench would likely catch it).

See #39262 for someone wasting time undoing something that didn't need undoing because said thing wasn't explained by a comment.

[kbuzzard]

could you please leave comments in the code explaining what that reason is?

Done.

and it would be perfect if you also added the properly dualised comment near CommRing.toRing

You mean "near Field.toCommRing" and there is no explicit instance defined here -- Field extends CommRing as a preferred parent, which is exactly why we should be preferring it over the scenic route via EuclideanDomain.