Theorem AddMonoid.End.mulRight_eq_mulLeft_of_commute

Modification history

2023-12-18 04:53

Mathlib/Algebra/Group/Hom/Instances.lean

feat(RingTheory/NonUnitalSubsemiring): point-free statement of centrality (#9053) …

Deleted AddMonoid.End.mulRight_eq_mulLeft_of_commute View on Github →

2023-12-03 23:47

Mathlib/Algebra/Group/Hom/Instances.lean

refactor(Algebra/Group/Defs): Separate commutative and associative multiplication (addition) (#7060) …

Added AddMonoid.End.mulRight_eq_mulLeft_of_commute View on Github →