Def CentroidHom.starRingOfCommCentroidHom

Modification history

2026-04-09 03:01
Mathlib/Algebra/Star/CentroidHom.lean
chore(Algebra): use `IsMulCommutative` to spell `Std.Commutative (· * ·)` (#37448) …
Modified CentroidHom.starRingOfCommCentroidHomView on Github →
2024-07-30 05:32
Mathlib/Algebra/Star/CentroidHom.lean
feat(algebra/hom/centroid): Centre of the Centroid of a *-ring is a *-ring (#6595) …
Added CentroidHom.starRingOfCommCentroidHomView on Github →