Commit 2023-02-28 15:58 8f18c313

View on Github →

feat: port Algebra.Hom.NonUnitalAlg (#2414)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Hom/NonUnitalAlg.lean

added theorem AlgHom.coe_to_nonUnitalAlgHom

added def AlgHom.toNonUnitalAlgHom

added theorem AlgHom.toNonUnitalAlgHom_eq_coe

added def NonUnitalAlgHom.Simps.apply

added theorem NonUnitalAlgHom.coe_comp

added theorem NonUnitalAlgHom.coe_distribMulActionHom_mk

added theorem NonUnitalAlgHom.coe_injective

added theorem NonUnitalAlgHom.coe_inl

added theorem NonUnitalAlgHom.coe_inr

added theorem NonUnitalAlgHom.coe_inverse

added theorem NonUnitalAlgHom.coe_mk

added theorem NonUnitalAlgHom.coe_mulHom_mk

added theorem NonUnitalAlgHom.coe_one

added theorem NonUnitalAlgHom.coe_prod

added theorem NonUnitalAlgHom.coe_to_distribMulActionHom

added theorem NonUnitalAlgHom.coe_to_mulHom

added theorem NonUnitalAlgHom.coe_zero

added def NonUnitalAlgHom.comp

added theorem NonUnitalAlgHom.comp_apply

added theorem NonUnitalAlgHom.congr_fun

added theorem NonUnitalAlgHom.ext

added theorem NonUnitalAlgHom.ext_iff

added def NonUnitalAlgHom.fst

added theorem NonUnitalAlgHom.fst_prod

added def NonUnitalAlgHom.inl

added theorem NonUnitalAlgHom.inl_apply

added def NonUnitalAlgHom.inr

added theorem NonUnitalAlgHom.inr_apply

added def NonUnitalAlgHom.inverse

added theorem NonUnitalAlgHom.mk_coe

added theorem NonUnitalAlgHom.one_apply

added def NonUnitalAlgHom.prod

added def NonUnitalAlgHom.prodEquiv

added theorem NonUnitalAlgHom.prod_fst_snd

added def NonUnitalAlgHom.snd

added theorem NonUnitalAlgHom.snd_prod

added theorem NonUnitalAlgHom.toDistribMulActionHom_eq_coe

added theorem NonUnitalAlgHom.toFun_eq_coe

added theorem NonUnitalAlgHom.toMulHom_eq_coe

added theorem NonUnitalAlgHom.to_distribMulActionHom_injective

added theorem NonUnitalAlgHom.to_mulHom_injective

added theorem NonUnitalAlgHom.zero_apply

added structure NonUnitalAlgHom