Theorem StarAlgEquiv.toAlgEquiv_ofAlgEquiv

Modification history

2025-09-04 11:48

Mathlib/Algebra/Star/StarAlgHom.lean

feat(Algebra/Star/StarAlgHom): some API for `StarAlgEquiv` (#28881) …

Added StarAlgEquiv.toAlgEquiv_ofAlgEquiv View on Github →