Commit 2024-06-26 22:10 bb6ed229

View on Github →

feat(Algebra/Star/StarRingHom): Add non-unital star ring homomorphisms (#12924) Definitions and basic properties of non-unital star ring homomorphisms

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Star/StarAlgHom.lean

Created Mathlib/Algebra/Star/StarRingHom.lean

added def NonUnitalStarRingHom.Simps.apply

added theorem NonUnitalStarRingHom.coe_comp

added theorem NonUnitalStarRingHom.coe_copy

added theorem NonUnitalStarRingHom.coe_id

added theorem NonUnitalStarRingHom.coe_mk

added theorem NonUnitalStarRingHom.coe_one

added theorem NonUnitalStarRingHom.coe_toNonUnitalRingHom

added theorem NonUnitalStarRingHom.coe_zero

added def NonUnitalStarRingHom.comp

added theorem NonUnitalStarRingHom.comp_apply

added theorem NonUnitalStarRingHom.comp_assoc

added theorem NonUnitalStarRingHom.comp_id

added theorem NonUnitalStarRingHom.copy_eq

added theorem NonUnitalStarRingHom.ext

added theorem NonUnitalStarRingHom.id_comp

added theorem NonUnitalStarRingHom.mk_coe

added theorem NonUnitalStarRingHom.one_apply

added theorem NonUnitalStarRingHom.zero_apply

added structure NonUnitalStarRingHom

added def NonUnitalStarRingHomClass.toNonUnitalStarRingHom

added def StarRingEquiv.Simps.apply

added def StarRingEquiv.Simps.symm_apply

added theorem StarRingEquiv.apply_symm_apply

added theorem StarRingEquiv.coe_mk

added theorem StarRingEquiv.coe_ofBijective

added theorem StarRingEquiv.coe_refl

added theorem StarRingEquiv.coe_trans

added theorem StarRingEquiv.ext

added theorem StarRingEquiv.ext_iff

added theorem StarRingEquiv.invFun_eq_symm

added theorem StarRingEquiv.leftInverse_symm

added theorem StarRingEquiv.mk_coe

added theorem StarRingEquiv.ofBijective_apply

added def StarRingEquiv.ofStarRingHom

added def StarRingEquiv.refl

added theorem StarRingEquiv.refl_symm

added theorem StarRingEquiv.rightInverse_symm

added theorem StarRingEquiv.symm_apply_apply

added theorem StarRingEquiv.symm_bijective

added theorem StarRingEquiv.symm_mk

added theorem StarRingEquiv.symm_symm

added theorem StarRingEquiv.symm_trans_apply

added theorem StarRingEquiv.toRingEquiv_eq_coe

added def StarRingEquiv.trans

added theorem StarRingEquiv.trans_apply

added structure StarRingEquiv

added def StarRingEquivClass.toStarRingEquiv