Def CentroidHom.centerIsoCentroid

Modification history

2024-01-18 18:38

Mathlib/Algebra/Ring/CentroidHom.lean

feat(Algebra/Ring/CentroidHom): central iff mul op commute (#8663) …

Modified CentroidHom.centerIsoCentroid View on Github →

2023-12-04 15:55

Mathlib/Algebra/Ring/CentroidHom.lean

feat(Algebra/Hom/Centroid) : Homomorphism from centre into centroid (#7843) …

Added CentroidHom.centerIsoCentroid View on Github →