Commit 2023-01-17 08:53 631abdea

View on Github →

feat: port algebra.hom.centroid (#1325)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Hom/Centroid.lean

added theorem CentroidHom.add_apply

added theorem CentroidHom.cancel_left

added theorem CentroidHom.cancel_right

added theorem CentroidHom.coe_add

added theorem CentroidHom.coe_comp

added theorem CentroidHom.coe_comp_addMonoidHom

added theorem CentroidHom.coe_copy

added theorem CentroidHom.coe_id

added theorem CentroidHom.coe_int_cast

added theorem CentroidHom.coe_mul

added theorem CentroidHom.coe_nat_cast

added theorem CentroidHom.coe_neg

added theorem CentroidHom.coe_nsmul

added theorem CentroidHom.coe_one

added theorem CentroidHom.coe_sub

added theorem CentroidHom.coe_to_add_monoid_hom

added theorem CentroidHom.coe_to_add_monoid_hom_injective

added theorem CentroidHom.coe_zero

added def CentroidHom.commRing

added def CentroidHom.comp

added theorem CentroidHom.comp_apply

added theorem CentroidHom.comp_assoc

added theorem CentroidHom.comp_id

added theorem CentroidHom.comp_mul_comm

added theorem CentroidHom.copy_eq

added theorem CentroidHom.ext

added theorem CentroidHom.id_apply

added theorem CentroidHom.id_comp

added theorem CentroidHom.int_cast_apply

added theorem CentroidHom.mul_apply

added theorem CentroidHom.nat_cast_apply

added theorem CentroidHom.neg_apply

added theorem CentroidHom.nsmul_apply

added theorem CentroidHom.one_apply

added theorem CentroidHom.sub_apply

added theorem CentroidHom.toAddMonoidHom_id

added def CentroidHom.toEnd

added theorem CentroidHom.toEnd_add

added theorem CentroidHom.toEnd_injective

added theorem CentroidHom.toEnd_int_cast

added theorem CentroidHom.toEnd_mul

added theorem CentroidHom.toEnd_nat_cast

added theorem CentroidHom.toEnd_neg

added theorem CentroidHom.toEnd_nsmul

added theorem CentroidHom.toEnd_one

added theorem CentroidHom.toEnd_pow

added theorem CentroidHom.toEnd_sub

added theorem CentroidHom.toEnd_zero

added theorem CentroidHom.toEnd_zsmul

added theorem CentroidHom.to_add_monoid_hom_eq_coe

added theorem CentroidHom.zero_apply

added structure CentroidHom