Theorem CentroidHom.center_iff_op_centroid

Modification history

2024-01-18 18:38
Mathlib/Algebra/Ring/CentroidHom.lean
feat(Algebra/Ring/CentroidHom): central iff mul op commute (#8663) …
Deleted CentroidHom.center_iff_op_centroidView on Github →
2023-12-04 15:55
Mathlib/Algebra/Ring/CentroidHom.lean
feat(Algebra/Hom/Centroid) : Homomorphism from centre into centroid (#7843) …
Added CentroidHom.center_iff_op_centroidView on Github →