Theorem NonUnitalNonAssocCommSemiring.mem_center_iff

Modification history

2024-01-18 18:38
Mathlib/Algebra/Ring/CentroidHom.lean
feat(Algebra/Ring/CentroidHom): central iff mul op commute (#8663) …
Added NonUnitalNonAssocCommSemiring.mem_center_iffView on Github →