Commit 2023-02-21 08:05 b4546c24

View on Github →

feat: port Algebra.Algebra.Hom (#2371)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Hom.lean

added def AlgHom.Simps.apply

added theorem AlgHom.algebraMap_eq_apply

added theorem AlgHom.coe_addMonoidHom_injective

added theorem AlgHom.coe_comp

added theorem AlgHom.coe_fn_inj

added theorem AlgHom.coe_fn_injective

added theorem AlgHom.coe_id

added theorem AlgHom.coe_mk'

added theorem AlgHom.coe_mk

added theorem AlgHom.coe_mks

added theorem AlgHom.coe_monoidHom_injective

added theorem AlgHom.coe_ringHom_injective

added theorem AlgHom.coe_ringHom_mk

added theorem AlgHom.coe_toAddMonoidHom

added theorem AlgHom.coe_toMonoidHom

added theorem AlgHom.coe_toRingHom

added theorem AlgHom.commutes

added def AlgHom.comp

added theorem AlgHom.comp_algebraMap

added theorem AlgHom.comp_apply

added theorem AlgHom.comp_assoc

added theorem AlgHom.comp_id

added theorem AlgHom.comp_toLinearMap

added theorem AlgHom.comp_toRingHom

added theorem AlgHom.ext

added theorem AlgHom.ext_iff

added theorem AlgHom.id_apply

added theorem AlgHom.id_comp

added theorem AlgHom.id_toRingHom

added theorem AlgHom.map_list_prod

added theorem AlgHom.map_smul_of_tower

added def AlgHom.mk'

added theorem AlgHom.mk_coe

added theorem AlgHom.mul_apply

added def AlgHom.ofLinearMap

added theorem AlgHom.ofLinearMap_id

added theorem AlgHom.ofLinearMap_toLinearMap

added theorem AlgHom.one_apply

added def AlgHom.toAddMonoidHom'

added theorem AlgHom.toFun_eq_coe

added def AlgHom.toLinearMap

added theorem AlgHom.toLinearMap_apply

added theorem AlgHom.toLinearMap_id

added theorem AlgHom.toLinearMap_injective

added theorem AlgHom.toLinearMap_ofLinearMap

added def AlgHom.toMonoidHom'

added theorem AlgHom.toRingHom_eq_coe

added theorem AlgHom.toRingHom_toRatAlgHom

added structure AlgHom

added def Algebra.ofId

added theorem Algebra.ofId_apply

added def MulSemiringAction.toAlgHom

added theorem MulSemiringAction.toAlgHom_injective

added def RingHom.equivRatAlgHom

added def RingHom.toIntAlgHom

added def RingHom.toNatAlgHom

added def RingHom.toRatAlgHom

added theorem RingHom.toRatAlgHom_toRingHom