Commit 2023-03-04 08:59 7ebff267

View on Github →

feat: port Algebra.Star.StarAlgHom (#2603)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Hom.lean

added def AlgHomClass.toAlgHom

Created Mathlib/Algebra/Star/StarAlgHom.lean

added def NonUnitalStarAlgHom.Simps.apply

added theorem NonUnitalStarAlgHom.coe_comp

added theorem NonUnitalStarAlgHom.coe_copy

added theorem NonUnitalStarAlgHom.coe_id

added theorem NonUnitalStarAlgHom.coe_inl

added theorem NonUnitalStarAlgHom.coe_inr

added theorem NonUnitalStarAlgHom.coe_mk

added theorem NonUnitalStarAlgHom.coe_one

added theorem NonUnitalStarAlgHom.coe_prod

added theorem NonUnitalStarAlgHom.coe_toNonUnitalAlgHom

added theorem NonUnitalStarAlgHom.coe_zero

added def NonUnitalStarAlgHom.comp

added theorem NonUnitalStarAlgHom.comp_apply

added theorem NonUnitalStarAlgHom.comp_assoc

added theorem NonUnitalStarAlgHom.comp_id

added theorem NonUnitalStarAlgHom.copy_eq

added theorem NonUnitalStarAlgHom.ext

added def NonUnitalStarAlgHom.fst

added theorem NonUnitalStarAlgHom.fst_prod

added theorem NonUnitalStarAlgHom.id_comp

added def NonUnitalStarAlgHom.inl

added theorem NonUnitalStarAlgHom.inl_apply

added def NonUnitalStarAlgHom.inr

added theorem NonUnitalStarAlgHom.inr_apply

added theorem NonUnitalStarAlgHom.mk_coe

added theorem NonUnitalStarAlgHom.one_apply

added def NonUnitalStarAlgHom.prod

added def NonUnitalStarAlgHom.prodEquiv

added theorem NonUnitalStarAlgHom.prod_fst_snd

added def NonUnitalStarAlgHom.snd

added theorem NonUnitalStarAlgHom.snd_prod

added theorem NonUnitalStarAlgHom.zero_apply

added structure NonUnitalStarAlgHom

added def StarAlgEquiv.Simps.apply

added def StarAlgEquiv.Simps.symm_apply

added theorem StarAlgEquiv.apply_symm_apply

added theorem StarAlgEquiv.coe_ofBijective

added theorem StarAlgEquiv.coe_refl

added theorem StarAlgEquiv.coe_trans

added theorem StarAlgEquiv.ext

added theorem StarAlgEquiv.ext_iff

added theorem StarAlgEquiv.invFun_eq_symm

added theorem StarAlgEquiv.leftInverse_symm

added theorem StarAlgEquiv.mk_coe'

added theorem StarAlgEquiv.ofBijective_apply

added def StarAlgEquiv.ofStarAlgHom

added def StarAlgEquiv.refl

added theorem StarAlgEquiv.refl_symm

added theorem StarAlgEquiv.rightInverse_symm

added theorem StarAlgEquiv.symm_apply_apply

added theorem StarAlgEquiv.symm_bijective

added theorem StarAlgEquiv.symm_mk

added theorem StarAlgEquiv.symm_symm

added theorem StarAlgEquiv.symm_to_ringEquiv

added theorem StarAlgEquiv.symm_trans_apply

added theorem StarAlgEquiv.toRingEquiv_eq_coe

added theorem StarAlgEquiv.to_ringEquiv_symm

added def StarAlgEquiv.trans

added theorem StarAlgEquiv.trans_apply

added structure StarAlgEquiv

added def StarAlgHom.Simps.apply

added theorem StarAlgHom.coe_comp

added theorem StarAlgHom.coe_copy

added theorem StarAlgHom.coe_id

added theorem StarAlgHom.coe_mk

added theorem StarAlgHom.coe_prod

added theorem StarAlgHom.coe_toAlgHom

added theorem StarAlgHom.coe_toNonUnitalStarAlgHom

added def StarAlgHom.comp

added theorem StarAlgHom.comp_apply

added theorem StarAlgHom.comp_assoc

added theorem StarAlgHom.comp_id

added theorem StarAlgHom.copy_eq

added theorem StarAlgHom.ext

added def StarAlgHom.fst

added theorem StarAlgHom.fst_prod

added theorem StarAlgHom.id_comp

added theorem StarAlgHom.mk_coe

added def StarAlgHom.prod

added def StarAlgHom.prodEquiv

added theorem StarAlgHom.prod_fst_snd

added def StarAlgHom.snd

added theorem StarAlgHom.snd_prod

added def StarAlgHom.toNonUnitalStarAlgHom

added structure StarAlgHom