Commit 2025-09-04 11:48 88d650f7

View on Github →

feat(Algebra/Star/StarAlgHom): some API for StarAlgEquiv (#28881) Namely, this adds the definitions StarAlgEquiv.toAlgEquiv and StarAlgEquiv.ofAlgEquiv.

Estimated changes

Modified Mathlib/Algebra/Star/StarAlgHom.lean

added theorem StarAlgEquiv.coe_symm_toAlgEquiv

added theorem StarAlgEquiv.coe_toAlgEquiv

added def StarAlgEquiv.ofAlgEquiv

added theorem StarAlgEquiv.ofAlgEquiv_apply

added theorem StarAlgEquiv.ofAlgEquiv_symm

added theorem StarAlgEquiv.ofAlgEquiv_toAlgEquiv

deleted theorem StarAlgEquiv.symm_to_ringEquiv

added def StarAlgEquiv.toAlgEquiv

added theorem StarAlgEquiv.toAlgEquiv_injective

added theorem StarAlgEquiv.toAlgEquiv_ofAlgEquiv

added theorem StarAlgEquiv.toAlgEquiv_refl

added theorem StarAlgEquiv.toAlgEquiv_symm

added theorem StarAlgEquiv.toAlgEquiv_trans

added theorem StarAlgEquiv.toRingEquiv_symm

modified theorem StarAlgEquiv.to_ringEquiv_symm