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 d4d96de5f1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ IsCyclic.isMulCommutative
+ instance (priority := low) (M) [MulOne M] [IsMulCommutative M] :
+ isMulCommutative_iff_isLieAbelian
- IsCyclic.commutative
- IsQuadraticExtension.isMulCommutative_galoisGroup
- commGroup_isMulCommutative
- 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).

vihdzp · 2026-03-31T18:34:14Z

Mathlib/Algebra/Group/Defs.lean

+class IsAddCommutative (M : Type*) [Add M] : Prop where
+  is_comm : Std.Commutative (α := M) (· + ·)


The design here seems odd. Why nest typeclasses instead of doing something like this?

Suggested change

class IsAddCommutative (M : Type*) [Add M] : Prop where

is_comm : Std.Commutative (α := M) (· + ·)

abbrev IsAddCommutative (M : Type*) [Add M] : Prop :=

Std.Commutative (α := M) (· + ·)

Hmm https://github.com/leanprover-community/mathlib4/pull/23773/files#r2280929588
FWIW this was the reason this class was introduced.

Oh actually, won't this cause the same performance issues as ContravariantClass has, since TC-search will search through all Std.Commutative instances regardless of the operation?

Yes, I believe the point is exactly that we want to avoid the performance impact of the same class being parameterized over the function.

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.

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

		class IsAddCommutative (M : Type*) [Add M] : Prop where
		is_comm : Std.Commutative (α := M) (· + ·)

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 d4d96de5f1

Import changes for modified files

Declarations diff

Uh oh!

vihdzp Mar 31, 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 Apr 1, 2026

Choose a reason for hiding this comment

Uh oh!

j-loreaux Apr 1, 2026

Choose a reason for hiding this comment

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented Mar 31, 2026 •

edited

Loading

SnirBroshi Apr 1, 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