perf: increase prio of AddCommMonoid.toAddMonoid

[kbuzzard]

The idea is that to prove M is an additive monoid, then essentially always it's a good idea to try to prove that it's a commutative additive monoid. This is in stark contrast to multiplication, which is often not commutative.

This change will not make failures any slower, but it might make successes faster.

---

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for a869a59 against c669471 are in. There are significant results. @kbuzzard

• 🟥 main exited with code 1

No significant changes detected.

[github-actions]

PR summary 63bdd3cb0b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

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.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 63bdd3c).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 63bdd3cb0b
Reference commit 2800ac2bd3

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

[mattrobball]

I once did an experiment where I increased all the priorities of CommX.toX and it went well.

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for 9f4a236 against c669471 are in. There are significant results. @kbuzzard

• 🟥 main exited with code 1

No significant changes detected.

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for a36a26e against c669471 are in. There are significant results. @kbuzzard

• 🟥 main exited with code 1

No significant changes detected.

[kbuzzard]

!radar

(fingers crossed this time)

[leanprover-radar]

Benchmark results for ee743b8 against c669471 are in. There are significant results. @kbuzzard

• ✅ build//instructions: -298.0G (-0.17%)

Large changes (1✅)

• ✅ build/module/Mathlib.Algebra.Ring.CentroidHom//instructions: -11.0G (-26.92%)

Medium changes (12✅, 1🟥)

• ✅ build/module/Mathlib.Algebra.Algebra.NonUnitalHom//instructions: -4.8G (-14.87%) (reduced significance based on absolute threshold)
• ✅ build/module/Mathlib.Algebra.Algebra.NonUnitalSubalgebra//instructions: -7.5G (-9.75%)
• 🟥 build/module/Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators//instructions: +2.4G (+12.89%)
• ✅ build/module/Mathlib.Algebra.Category.ModuleCat.Stalk//instructions: -15.7G (-6.56%)
• ✅ build/module/Mathlib.Algebra.Module.LinearMap.Defs//instructions: -4.3G (-7.80%)
• ✅ build/module/Mathlib.Algebra.Star.LinearMap//instructions: -7.9G (-19.63%)
• ✅ build/module/Mathlib.Algebra.Star.StarAlgHom//instructions: -4.2G (-9.46%)
• ✅ build/module/Mathlib.Analysis.Calculus.FormalMultilinearSeries//instructions: -6.9G (-12.44%)
• ✅ build/module/Mathlib.LinearAlgebra.BilinearMap//instructions: -8.3G (-10.39%)
• ✅ build/module/Mathlib.LinearAlgebra.TensorProduct.Defs//instructions: -5.0G (-10.89%)
• ✅ build/module/Mathlib.LinearAlgebra.TensorProduct.Tower//instructions: -17.3G (-9.52%)
• ✅ build/module/Mathlib.RingTheory.Derivation.Basic//instructions: -4.0G (-7.87%)
• ✅ build/module/Mathlib.Topology.Algebra.Module.LinearMap//instructions: -8.4G (-7.14%)

Small changes (85✅, 29🟥)

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

[kbuzzard]

At the suggestion of Matt Ballard, I might try groups/rings too.

[kbuzzard]

!radar

[leanprover-radar]

Benchmark results for 63bdd3c against 2800ac2 are in. There are significant results. @kbuzzard

• ✅ build//instructions: -447.4G (-0.29%)

Large changes (1✅)

1 hidden

Medium changes (21✅)

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

Small changes (102✅, 20🟥)

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