Commit 2026-04-09 03:01 eee511db

View on Github →

chore(Algebra): use IsMulCommutative to spell Std.Commutative (· * ·) (#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.

Estimated changes

modified theorem isMulCommutative_iff
modified theorem IsAbelianGalois.of_isCyclic
modified theorem commProb_eq_one_iff
modified def IsCyclic.commGroup