Theorem StarAlgEquiv.to_ringEquiv_symm

Modification history

2026-03-25 05:05
Mathlib/Algebra/Star/StarAlgHom.lean
chore: remove declarations deprecated between 2021-03-24 and 2025-09-24 (#37118) …
Deleted StarAlgEquiv.to_ringEquiv_symmView on Github →
2025-09-04 11:48
Mathlib/Algebra/Star/StarAlgHom.lean
feat(Algebra/Star/StarAlgHom): some API for `StarAlgEquiv` (#28881) …
Modified StarAlgEquiv.to_ringEquiv_symmView on Github →
2023-03-04 08:59
Mathlib/Algebra/Star/StarAlgHom.lean
feat: port Algebra.Star.StarAlgHom (#2603)
Added StarAlgEquiv.to_ringEquiv_symmView on Github →