Theorem Set.mem_center_iff_addMonoidHom

Modification history

2023-12-18 04:53
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
feat(RingTheory/NonUnitalSubsemiring): point-free statement of centrality (#9053) …
Added Set.mem_center_iff_addMonoidHomView on Github →