Theorem AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute

Modification history

2024-04-20 06:50

Mathlib/Algebra/Group/Hom/End.lean

chore: refactor to avoid importing Ring for Group topics (#11913) …

Modified AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute View on Github →

2023-12-18 04:53

Mathlib/Algebra/Group/Hom/Instances.lean

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

Added AddMonoidHom.mulRight_eq_mulLeft_iff_forall_commute View on Github →