Theorem isMulCommutative_iff_isLieAbelian

Modification history

2026-04-09 03:01
Mathlib/Algebra/Lie/Abelian.lean
chore(Algebra): use `IsMulCommutative` to spell `Std.Commutative (· * ·)` (#37448) …
Added isMulCommutative_iff_isLieAbelianView on Github →