Commit 2025-11-15 13:02 377a3b70

View on Github →

refactor(Algebra/Star/StarAlgHom): let StarAlgEquiv extend StarRingEquiv instead of RingEquiv (#29347) Instead of having StarAlgEquiv extend RingEquiv and have properties map_star' and map_smul', it now extends StarRingEquiv with only map_smul'.

Estimated changes

Modified Mathlib/Algebra/Star/StarAlgHom.lean

modified theorem StarAlgEquiv.coe_mk

added theorem StarAlgEquiv.toStarRingEquiv_eq_coe

added theorem StarAlgEquiv.toStarRingEquiv_symm

Modified Mathlib/Algebra/Star/StarRingHom.lean

modified theorem StarRingEquiv.coe_mk

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean