chore: try more expanded ring definition

[sgouezel]

---

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

[github-actions]

PR summary f369f66ea0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Ring.toAddGroupWithOne'

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.09)

Current number	Change	Type
11	1	maxHeartBeats modifications

Current commit 8a412f16d1
Reference commit f369f66ea0

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[sgouezel]

!radar

[leanprover-radar]

Benchmark results for 816a90f against f369f66 are in. There are significant results. @sgouezel

• 🟥 build//instructions: +742.7G (+0.43%)

Large changes (5🟥)

• 🟥 build/module/Mathlib.Algebra.Order.Ring.StandardPart//instructions: +40.7G (+24.60%)
• 🟥 build/module/Mathlib.AlgebraicGeometry.GammaSpecAdjunction//instructions: +33.2G (+34.99%)
• 🟥 build/module/Mathlib.NumberTheory.NumberField.Completion.InfinitePlace//instructions: +9.7G (+17.82%)
• 🟥 build/module/Mathlib.NumberTheory.Padics.HeightOneSpectrum//instructions: +17.8G (+22.41%)
• 🟥 build/module/Mathlib.RingTheory.DedekindDomain.AdicValuation//instructions: +35.0G (+26.69%)

Medium changes (22🟥)

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

Small changes (6✅, 78🟥)

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

[JovanGerb]

By the way, you can change the priority of the instance generated by extends (in the same way that I did in #37962). Maybe this will fix it.

[sgouezel]

!radar

[leanprover-radar]

Benchmark results for c911b05 against f369f66 are in. There are significant results. @sgouezel

• 🟥 build//instructions: +439.7G (+0.26%)

Medium changes (1✅, 6🟥)

• ✅ build/module/Mathlib.Algebra.Category.ModuleCat.Stalk//instructions: -7.4G (-3.14%)
• 🟥 build/module/Mathlib.Algebra.Order.Ring.StandardPart//instructions: +21.7G (+13.15%)
• 🟥 build/module/Mathlib.NumberTheory.NumberField.Completion.InfinitePlace//instructions: +3.9G (+7.23%)
• 🟥 build/module/Mathlib.NumberTheory.Padics.HeightOneSpectrum//instructions: +5.2G (+6.58%)
• 🟥 build/module/Mathlib.NumberTheory.Padics.WithVal//instructions: +2.4G (+5.54%)
• 🟥 build/module/Mathlib.RingTheory.DedekindDomain.AdicValuation//instructions: +7.5G (+5.68%)
• 🟥 build/module/Mathlib.RingTheory.QuotSMulTop//instructions: +7.3G (+21.66%)

Small changes (4✅, 37🟥)

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