Theorem StarAlgEquiv.toRingEquiv_symm

Modification history

2026-09-08 20:38
Mathlib/Algebra/Star/StarAlgHom.lean
chore: remove coercion attribute from `{NonUnitalStarRingHom, StarRingEquiv}.ofClass` (#43393) …
Modified StarAlgEquiv.toRingEquiv_symmView on Github →
2026-04-13 10:18
Mathlib/Algebra/Star/StarAlgHom.lean
refactor(Algebra): replace `RingEquivClass.toRingEquiv` by structure-specific coercions (#21031) …
Modified StarAlgEquiv.toRingEquiv_symmView on Github →
2025-09-04 11:48
Mathlib/Algebra/Star/StarAlgHom.lean
feat(Algebra/Star/StarAlgHom): some API for `StarAlgEquiv` (#28881) …
Added StarAlgEquiv.toRingEquiv_symmView on Github →