Commit 2024-07-30 05:32 38c577df
View on Github →feat(algebra/hom/centroid): Centre of the Centroid of a *-ring is a *-ring (#6595) This PR shows that the centre of the centroid of a *-ring is a *-ring. Previously submitted to mathlib as https://github.com/leanprover-community/mathlib/pull/18096