[Merged by Bors] - chore(Algebra): use `IsMulCommutative` to spell `Std.Commutative (· * ·)` by SnirBroshi · Pull Request #37448 · leanprover-community/mathlib4

SnirBroshi · 2026-03-31T17:10:56Z

and use IsAddCommutative to spell Std.Commutative (· + ·).

Also makes Is{Mul/Add}Commutative.is_comm instances so that core lemmas (or grind) can synthesize Std.Commutative.

Hopefully this is useful since #36549 was merged.

… ·)`

github-actions · 2026-03-31T17:12:04Z

PR summary 5d32f3eac7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsAddCyclic.commutative
+ IsCyclic.isMulCommutative
+ instance (priority := low) (M) [MulOne M] [IsMulCommutative M] :
+ isMulCommutative_iff_isLieAbelian
- instance (priority := low) (M) [MulOne M] [Std.Commutative (α := M) (· * ·)] :
- instance [Group G] (H : Subgroup G) [IsCyclic H] : IsMulCommutative H

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.

No changes to technical debt.

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).

Mathlib/Algebra/Group/Defs.lean

Mathlib/Algebra/Lie/Abelian.lean

Mathlib/GroupTheory/SpecificGroups/Cyclic/Basic.lean

…ff_isLieAbelian`

SnirBroshi · 2026-04-01T01:03:31Z

!bench

leanprover-radar · 2026-04-01T01:03:55Z

Benchmark results for 6d77e2a against d4d96de are in. There are no significant changes. @SnirBroshi

🟥 build//instructions: +36.5G (+0.02%)

Medium changes (1🟥)

🟥 build/module/Mathlib.GroupTheory.SchurZassenhaus//instructions: +3.9G (+24.41%)

Small changes (5🟥)

🟥 build/module/Mathlib.Data.ZMod.QuotientGroup//instructions: +1.0G (+5.81%)
🟥 build/module/Mathlib.GroupTheory.Focal//instructions: +2.5G (+15.07%)
🟥 build/module/Mathlib.GroupTheory.Schreier//instructions: +917.7M (+6.14%)
🟥 build/module/Mathlib.RepresentationTheory.AlgebraRepresentation.Basic//instructions: +915.0M (+10.59%)
🟥 build/module/Mathlib.Topology.Algebra.StarSubalgebra//instructions: +3.0G (+13.32%)

j-loreaux · 2026-04-01T02:09:39Z

Mathlib/Algebra/Group/Hom/Defs.lean

    obtain ⟨b', hb'⟩ := is_surj b
    simp only [← ha', ← hb', ← map_mul]
-    rw [is_comm.comm]
+    rw [is_comm.is_comm.comm]


Can you not use mul_comm' here (and everywhere else)?

Done except for SpecificGroups/Dihedral.lean where it can't easily infer the type,
and h'.is_comm.comm (r 1) (sr 0) seems better than mul_comm' (r (n := n + 3) 1) (sr 0)

SnirBroshi · 2026-04-01T07:30:56Z

Just testing the abbrev version, I'm interested in seeing the performance

!bench

leanprover-radar · 2026-04-01T07:31:28Z

Benchmark results for 0c2121f against d4d96de are in. There are no significant changes. @SnirBroshi

🟥 build//instructions: +39.3G (+0.02%)

Medium changes (2🟥)

🟥 build/module/Mathlib.GroupTheory.SchurZassenhaus//instructions: +5.3G (+32.73%)
🟥 build/module/Mathlib.RepresentationTheory.AlgebraRepresentation.Basic//instructions: +2.2G (+25.15%)

Small changes (1✅, 6🟥)

🟥 build/module/Mathlib.Algebra.Star.Subalgebra//instructions: +2.6G (+4.09%)
✅ build/module/Mathlib.CategoryTheory.Limits.Types.Coequalizers//instructions: -373.4M (-5.81%)
🟥 build/module/Mathlib.Data.ZMod.QuotientGroup//instructions: +1.7G (+9.71%)
🟥 build/module/Mathlib.GroupTheory.Focal//instructions: +3.1G (+18.84%)
🟥 build/module/Mathlib.GroupTheory.Schreier//instructions: +1.1G (+7.35%)
🟥 build/module/Mathlib.Lean.Meta.Basic//instructions: +143.6M (+3.70%)
🟥 build/module/Mathlib.Topology.Algebra.StarSubalgebra//instructions: +4.8G (+21.58%)

SnirBroshi · 2026-04-01T10:05:57Z

Hmm switching to abbrev seems to have basically the same performance, maybe we don't have enough Std.Commutative instances to see the issue?
In any case I reverted back to a one-field class.

tb65536 · 2026-04-06T10:32:29Z

!radar

leanprover-radar · 2026-04-06T10:32:49Z

Benchmark results for 7292add against d4d96de are in. There are no significant changes. @tb65536

🟥 build//instructions: +42.3G (+0.02%)

Medium changes (2🟥)

🟥 build/module/Mathlib.GroupTheory.Focal//instructions: +2.2G (+13.08%)
🟥 build/module/Mathlib.GroupTheory.SchurZassenhaus//instructions: +3.8G (+23.93%)

Small changes (4🟥)

🟥 build/module/Mathlib.Data.ZMod.QuotientGroup//instructions: +1.0G (+5.80%)
🟥 build/module/Mathlib.GroupTheory.Schreier//instructions: +815.8M (+5.46%)
🟥 build/module/Mathlib.RepresentationTheory.AlgebraRepresentation.Basic//instructions: +857.1M (+9.92%)
🟥 build/module/Mathlib.Topology.Algebra.StarSubalgebra//instructions: +2.5G (+11.35%)

leanprover-radar · 2026-04-06T22:20:59Z

Benchmark results for c687a3d against de14307 are in. Significant changes detected! @tb65536

🟥 main exited with code 1

No significant changes detected.

SnirBroshi · 2026-04-07T18:10:25Z

!bench

leanprover-radar · 2026-04-07T18:10:45Z

Benchmark results for c687a3d against de14307 are in. Significant changes detected! @SnirBroshi

🟥 main exited with code 1

No significant changes detected.

…mmutative

SnirBroshi · 2026-04-07T22:20:38Z

!bench

leanprover-radar · 2026-04-07T22:20:55Z

Benchmark results for 98005e1 against 5d32f3e are in. There are no significant changes. @SnirBroshi

🟥 build//instructions: +17.2G (+0.01%)

Medium changes (2🟥)

🟥 build/module/Mathlib.GroupTheory.Focal//instructions: +2.1G (+12.93%)
🟥 build/module/Mathlib.GroupTheory.SchurZassenhaus//instructions: +3.6G (+22.63%)

Small changes (1✅, 4🟥)

🟥 build/module/Mathlib.Algebra.Module.Torsion.Free//instructions: +669.6M (+6.07%)
🟥 build/module/Mathlib.Analysis.InnerProductSpace.Harmonic.Basic//instructions: +437.0M (+3.26%)
🟥 build/module/Mathlib.GroupTheory.Schreier//instructions: +665.7M (+4.57%)
🟥 build/module/Mathlib.RepresentationTheory.AlgebraRepresentation.Basic//instructions: +809.1M (+9.52%)
✅ build/module/Mathlib.Tactic.Linarith//instructions: -264.9M (-5.85%)

tb65536

Thanks!

maintainer merge

github-actions · 2026-04-08T09:48:02Z

🚀 Pull request has been placed on the maintainer queue by tb65536.

Mathlib/GroupTheory/SpecificGroups/Cyclic/Basic.lean

Mathlib/FieldTheory/Galois/Basic.lean

Mathlib/Algebra/Group/Subgroup/Defs.lean

SnirBroshi · 2026-04-09T02:26:26Z

Oh sorry, I thought we never add deprecations to instances, even explicitly named ones. Added!

adomani

Thanks!

Regarding the deprecations, I am probably being overcareful, but when you are proving that a group is commutative, you are more likely to call on an instance explicitly inside a proof. In such situations, the deprecations are helpful.

bors merge

… ·)` (#37448) and use `IsAddCommutative` to spell `Std.Commutative (· + ·)`. Also makes `Is{Mul/Add}Commutative.is_comm` instances so that core lemmas (or `grind`) can synthesize `Std.Commutative`.

mathlib-bors · 2026-04-09T04:02:40Z

Pull request successfully merged into master.

Build succeeded:

…heorem Corrects a mistake I made in leanprover-community#37448

SnirBroshi · 2026-04-09T04:27:11Z

Mathlib/FieldTheory/Galois/Basic.lean

+@[deprecated inferInstance (since := "2026-04-09")]
+instance IsQuadraticExtension.isMulCommutative_galoisGroup : IsMulCommutative Gal(K/F) :=
+  inferInstance


Oops, sorry, #37822

…heorem (#37822) Corrects a mistake I made in #37448

… ·)` (leanprover-community#37448) and use `IsAddCommutative` to spell `Std.Commutative (· + ·)`. Also makes `Is{Mul/Add}Commutative.is_comm` instances so that core lemmas (or `grind`) can synthesize `Std.Commutative`.

…heorem (leanprover-community#37822) Corrects a mistake I made in leanprover-community#37448

chore(Algebra): use IsMulCommutative to spell `Std.Commutative (· *…

6054c4c

… ·)`

github-actions bot added the t-group-theory Group theory label Mar 31, 2026

vihdzp reviewed Mar 31, 2026

View reviewed changes

SnirBroshi added 5 commits April 1, 2026 02:59

fix GroupTheory/Focal and FieldTheory/Galois/Basic

9f798ec

delete redundant instances

5855d5b

rename IsCyclic.commutative -> IsCyclic.isMulCommutative

5643fb3

rename commutative_ring_iff_abelian_lie_ring -> `isMulCommutative_i…

9658ebe

…ff_isLieAbelian`

fix rename IsCyclic.commutative -> IsCyclic.isMulCommutative

6d77e2a

mathlib-triage bot assigned tb65536 Apr 1, 2026

j-loreaux reviewed Apr 1, 2026

View reviewed changes

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 1, 2026

SnirBroshi added 6 commits April 1, 2026 05:35

delete another redundant instance

b0ec876

use scoped instance for IsCyclic.commGroup in Cyclic/Basic

8523a08

delete redundant have

210b169

try the abbrev refactor

d87eca7

fix

bf22a28

more fixes

0c2121f

SnirBroshi added 3 commits April 1, 2026 12:05

Revert the last 3 commits (0c2121f bf22a28 d87eca7)

4ff636d

cleanup

4f19559

IsMulCommutative.is_comm.comm -> mul_comm'

7292add

SnirBroshi removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 1, 2026

SnirBroshi requested a review from j-loreaux April 1, 2026 11:29

Merge branch 'master' into chore/algebra/std-commutative-to-is-mul-co…

98005e1

…mmutative

SnirBroshi requested review from tb65536 and removed request for tb65536 April 7, 2026 23:46

tb65536 approved these changes Apr 8, 2026

View reviewed changes

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 8, 2026

adomani reviewed Apr 8, 2026

View reviewed changes

Mathlib/GroupTheory/SpecificGroups/Cyclic/Basic.lean Show resolved Hide resolved

adomani reviewed Apr 8, 2026

View reviewed changes

Mathlib/FieldTheory/Galois/Basic.lean Show resolved Hide resolved

adomani reviewed Apr 8, 2026

View reviewed changes

Mathlib/Algebra/Group/Subgroup/Defs.lean Show resolved Hide resolved

add deprecations

22cbbfd

SnirBroshi requested a review from adomani April 9, 2026 02:26

adomani reviewed Apr 9, 2026

View reviewed changes

mathlib-triage bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 9, 2026

mathlib-bors bot changed the title ~~chore(Algebra): use IsMulCommutative to spell Std.Commutative (· * ·)~~ [Merged by Bors] - chore(Algebra): use IsMulCommutative to spell Std.Commutative (· * ·) Apr 9, 2026

mathlib-bors bot closed this Apr 9, 2026

SnirBroshi added a commit to SnirBroshi/mathlib4 that referenced this pull request Apr 9, 2026

fix(FieldTheory/Galois/Basic): inferInstance instance should be a t…

d7604e4

…heorem Corrects a mistake I made in leanprover-community#37448

SnirBroshi mentioned this pull request Apr 9, 2026

[Merged by Bors] - fix(FieldTheory/Galois/Basic): inferInstance instance should be a theorem #37822

Closed

SnirBroshi commented Apr 9, 2026

View reviewed changes

mathlib-bors bot pushed a commit that referenced this pull request Apr 9, 2026

fix(FieldTheory/Galois/Basic): inferInstance instance should be a t…

4ecbd99

…heorem (#37822) Corrects a mistake I made in #37448

xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Apr 10, 2026

fix(FieldTheory/Galois/Basic): inferInstance instance should be a t…

6741ee8

…heorem (leanprover-community#37822) Corrects a mistake I made in leanprover-community#37448

Conversation

SnirBroshi commented Mar 31, 2026

Uh oh!

github-actions bot commented Mar 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5d32f3eac7

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SnirBroshi commented Apr 1, 2026

Uh oh!

leanprover-radar commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

j-loreaux Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

SnirBroshi Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

SnirBroshi commented Apr 1, 2026

Uh oh!

leanprover-radar commented Apr 1, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SnirBroshi commented Apr 1, 2026

Uh oh!

tb65536 commented Apr 6, 2026

Uh oh!

leanprover-radar commented Apr 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

leanprover-radar commented Apr 6, 2026

Uh oh!

SnirBroshi commented Apr 7, 2026

Uh oh!

leanprover-radar commented Apr 7, 2026

Uh oh!

SnirBroshi commented Apr 7, 2026

Uh oh!

leanprover-radar commented Apr 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

tb65536 left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Apr 8, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

SnirBroshi commented Apr 9, 2026

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Apr 9, 2026

Uh oh!

SnirBroshi Apr 9, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions bot commented Mar 31, 2026 •

edited

Loading

leanprover-radar commented Apr 1, 2026 •

edited

Loading

SnirBroshi Apr 1, 2026 •

edited

Loading

leanprover-radar commented Apr 1, 2026 •

edited

Loading

leanprover-radar commented Apr 6, 2026 •

edited

Loading

leanprover-radar commented Apr 7, 2026 •

edited

Loading