Theorem AddMonoid.End.comm_mulRight_eq_mulLeft

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.comm_mulRight_eq_mulLeftView 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.comm_mulRight_eq_mulLeftView on Github →