Def StarAlgEquivClass.toStarAlgEquiv

Modification history

2026-09-07 13:06
Mathlib/Algebra/Star/StarAlgHom.lean
chore: standardise names for coercions from morphism classes to morphisms (#43367) …
Deleted StarAlgEquivClass.toStarAlgEquivView on Github →
2024-02-14 12:29
Mathlib/Algebra/Star/StarAlgHom.lean
feat: add the coercion from types satisfying `StarAlgEquivClass` to `StarAlgEquiv` (#10368)
Added StarAlgEquivClass.toStarAlgEquivView on Github →