Def CentroidHom.centerToCentroid

Modification history

2024-07-30 05:32
Mathlib/Algebra/Ring/CentroidHom.lean
feat(algebra/hom/centroid): Centre of the Centroid of a *-ring is a *-ring (#6595) …
Modified CentroidHom.centerToCentroidView on Github →
2023-12-04 15:55
Mathlib/Algebra/Ring/CentroidHom.lean
feat(Algebra/Hom/Centroid) : Homomorphism from centre into centroid (#7843) …
Added CentroidHom.centerToCentroidView on Github →