Commit 2026-09-08 20:38 b7f093a3
View on Github →chore: remove coercion attribute from {NonUnitalStarRingHom, StarRingEquiv}.ofClass (#43393)
As discussed in #31365, this is the final step of fixing the morphism design for these classes.
Add a missing definition and coercion for StarRingEquiv.toNonUnitalStarRingHom.