Theorem CentroidHom.starCenterIsoCentroid_symm_apply_coe

Modification history

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.starCenterIsoCentroid_symm_apply_coeView on Github →