Commit 2026-09-09 10:11 754ac8a5

View on Github →

chore: remove coercion attribute from StarAlgEquiv.ofClass (#43370) As discussed in #31365, this is the final step of fixing the morphism design for this class.

Estimated changes

Modified Mathlib/Algebra/Algebra/Unitization.lean

Modified Mathlib/Algebra/Star/NonUnitalSubalgebra.lean

Modified Mathlib/Algebra/Star/StarAlgHom.lean

Modified Mathlib/Algebra/Star/Subalgebra.lean

modified theorem StarAlgHom.ext_of_adjoin_eq_top

Modified Mathlib/Analysis/CStarAlgebra/Commutative/PosPart.lean

Modified Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Restrict.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

Modified Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

Modified Mathlib/Analysis/CStarAlgebra/Hom.lean

Modified Mathlib/Analysis/CStarAlgebra/Spectrum.lean

Modified Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean

Modified Mathlib/Topology/Algebra/StarSubalgebra.lean