CentroidHom

📁 Source: Mathlib/Algebra/Ring/CentroidHom.lean

Statistics

Metric	Count
Definitions `applyModule`, `centerIsoCentroid`, `centerToCentroid`, `centerToCentroidCenter`, `commRing`, `comp`, `copy`, `hasNPowNat`, `id`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instDistribMulAction`, `instFunLike`, `instFunLikeSubtypeMemSubsemiringCenter`, `instInhabited`, `instIntCast`, `instModule`, `instMul`, `instNatCast`, `instNeg`, `instOne`, `instRing`, `instSMul`, `instSemiring`, `instSub`, `instZero`, `toAddMonoidHom`, `toEnd`, `toEndRingHom`, `CentroidHomClass`, `toCentroidHom`, `instCoeTCCentroidHomOfCentroidHomClass`	33
Theorems `add_apply`, `cancel_left`, `cancel_right`, `centerToCentroidCenter_apply`, `centerToCentroid_apply`, `centroid_eq_centralizer_mulLeftRight`, `coe_add`, `coe_comp`, `coe_comp_addMonoidHom`, `coe_copy`, `coe_id`, `coe_intCast`, `coe_mul`, `coe_natCast`, `coe_neg`, `coe_one`, `coe_smul`, `coe_sub`, `coe_toAddMonoidHom`, `coe_toAddMonoidHom_injective`, `coe_zero`, `comp_apply`, `comp_assoc`, `comp_id`, `comp_mul_comm`, `copy_eq`, `ext`, `ext_iff`, `id_apply`, `id_comp`, `instCentroidHomClass`, `instIsCentralScalar`, `instIsScalarTower`, `instIsScalarTower_1`, `instSMulCommClass`, `instSMulCommClass_1`, `instSMulCommClass_2`, `intCast_apply`, `isScalarTowerRight`, `map_mul_left'`, `map_mul_right'`, `mul_apply`, `natCast_apply`, `neg_apply`, `one_apply`, `smul_apply`, `smul_def`, `sub_apply`, `toAddMonoidHom_eq_coe`, `toAddMonoidHom_id`, `toEndRingHom_apply`, `toEnd_add`, `toEnd_injective`, `toEnd_intCast`, `toEnd_mul`, `toEnd_natCast`, `toEnd_neg`, `toEnd_one`, `toEnd_pow`, `toEnd_smul`, `toEnd_sub`, `toEnd_zero`, `toFun_eq_coe`, `zero_apply`, `map_mul_left`, `map_mul_right`, `toAddMonoidHomClass`, `toCentroidHom_apply_toFun`, `mem_center_iff`, `mem_center_iff`	70
Total	103

CentroidHom

Definitions

Name	Category	Theorems
`applyModule` 📖	CompOp	4 math math: `smul_def`, `instSMulCommClass_2`, `instSMulCommClass_1`, `instIsScalarTower_1`
`centerIsoCentroid` 📖	CompOp	—
`centerToCentroid` 📖	CompOp	1 math math: `centerToCentroid_apply`
`centerToCentroidCenter` 📖	CompOp	2 math math: `star_centerToCentroidCenter`, `centerToCentroidCenter_apply`
`commRing` 📖	CompOp	—
`comp` 📖	CompOp	8 math math: `comp_id`, `cancel_right`, `id_comp`, `comp_apply`, `coe_comp`, `cancel_left`, `comp_assoc`, `coe_comp_addMonoidHom`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`hasNPowNat` 📖	CompOp	1 math math: `toEnd_pow`
`id` 📖	CompOp	7 math math: `comp_id`, `id_comp`, `toAddMonoidHom_id`, `coe_intCast`, `coe_id`, `id_apply`, `coe_natCast`
`instAdd` 📖	CompOp	5 math math: `starCenterIsoCentroid_symm_apply_coe`, `starCenterIsoCentroid_apply`, `coe_add`, `toEnd_add`, `add_apply`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	—
`instDistribMulAction` 📖	CompOp	—
`instFunLike` 📖	CompOp	37 math math: `starCenterIsoCentroid_symm_apply_coe`, `zero_apply`, `coe_toAddMonoidHom`, `natCast_apply`, `smul_def`, `coe_add`, `neg_apply`, `sub_apply`, `star_apply`, `smul_apply`, `toAddMonoidHom_id`, `coe_intCast`, `coe_sub`, `coe_one`, `coe_neg`, `coe_id`, `Module.toCentroidHom_apply_toFun`, `ext_iff`, `comp_apply`, `add_apply`, `id_apply`, `coe_comp`, `instCentroidHomClass`, `coe_toAddMonoidHom_injective`, `toFun_eq_coe`, `comp_mul_comm`, `coe_zero`, `mul_apply`, `toAddMonoidHom_eq_coe`, `coe_comp_addMonoidHom`, `coe_smul`, `centerToCentroid_apply`, `starCenterToCentroid_apply`, `intCast_apply`, `one_apply`, `coe_natCast`, `coe_mul`
`instFunLikeSubtypeMemSubsemiringCenter` 📖	CompOp	1 math math: `centerToCentroidCenter_apply`
`instInhabited` 📖	CompOp	—
`instIntCast` 📖	CompOp	3 math math: `toEnd_intCast`, `coe_intCast`, `intCast_apply`
`instModule` 📖	CompOp	—
`instMul` 📖	CompOp	6 math math: `starCenterIsoCentroid_symm_apply_coe`, `starCenterIsoCentroid_apply`, `mul_apply`, `toEnd_mul`, `isScalarTowerRight`, `coe_mul`
`instNatCast` 📖	CompOp	3 math math: `natCast_apply`, `toEnd_natCast`, `coe_natCast`
`instNeg` 📖	CompOp	3 math math: `neg_apply`, `coe_neg`, `toEnd_neg`
`instOne` 📖	CompOp	3 math math: `toEnd_one`, `coe_one`, `one_apply`
`instRing` 📖	CompOp	—
`instSMul` 📖	CompOp	7 math math: `toEnd_smul`, `smul_apply`, `instIsScalarTower`, `instSMulCommClass`, `instIsCentralScalar`, `coe_smul`, `isScalarTowerRight`
`instSemiring` 📖	CompOp	13 math math: `star_centerToCentroidCenter`, `starCenterIsoCentroid_apply`, `smul_def`, `centroid_eq_centralizer_mulLeftRight`, `instSMulCommClass_2`, `Module.toCentroidHom_apply_toFun`, `instSMulCommClass_1`, `instIsScalarTower_1`, `toEndRingHom_apply`, `NonUnitalNonAssocSemiring.mem_center_iff`, `centerToCentroidCenter_apply`, `centerToCentroid_apply`, `starCenterToCentroid_apply`
`instSub` 📖	CompOp	3 math math: `toEnd_sub`, `sub_apply`, `coe_sub`
`instZero` 📖	CompOp	3 math math: `zero_apply`, `toEnd_zero`, `coe_zero`
`toAddMonoidHom` 📖	CompOp	4 math math: `map_mul_left'`, `toFun_eq_coe`, `toAddMonoidHom_eq_coe`, `map_mul_right'`
`toEnd` 📖	CompOp	12 math math: `toEnd_pow`, `toEnd_sub`, `toEnd_one`, `toEnd_smul`, `toEnd_add`, `toEnd_intCast`, `toEnd_natCast`, `toEnd_zero`, `toEndRingHom_apply`, `toEnd_injective`, `toEnd_mul`, `toEnd_neg`
`toEndRingHom` 📖	CompOp	3 math math: `centroid_eq_centralizer_mulLeftRight`, `toEndRingHom_apply`, `NonUnitalNonAssocSemiring.mem_center_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`cancel_left` 📖	mathematical	`DFunLike.coe` `CentroidHom` `instFunLike`	`comp`	—	`ext` `comp_apply`
`cancel_right` 📖	mathematical	`DFunLike.coe` `CentroidHom` `instFunLike`	`comp`	—	`ext` `Function.Surjective.forall` `DFunLike.ext_iff`
`centerToCentroidCenter_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `Subsemiring` `Semiring.toNonAssocSemiring` `instSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.center` `instFunLikeSubtypeMemSubsemiringCenter` `NonUnitalRingHom` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instSetLike` `NonUnitalSubsemiring.center` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalSubsemiring.center.instNonUnitalCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.toNonAssocSemiring` `NonUnitalRingHom.instFunLike` `centerToCentroidCenter` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`centerToCentroid_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `NonUnitalRingHom` `NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `NonUnitalSubsemiring.center` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalSubsemiring.center.instNonUnitalCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `NonUnitalRingHom.instFunLike` `centerToCentroid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`centroid_eq_centralizer_mulLeftRight` 📖	mathematical	—	`RingHom.rangeS` `CentroidHom` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toNonAssocSemiring` `instSemiring` `AddMonoid.End.instSemiring` `toEndRingHom` `Subsemiring.centralizer` `Set` `Set.instUnion` `Set.range` `DFunLike.coe` `AddMonoidHom` `AddMonoid.End.instAddCommMonoid` `AddMonoidHom.instFunLike` `AddMonoid.End.mulLeft` `AddMonoid.End.mulRight`	—	`Subsemiring.ext` `AddMonoidHom.ext` `CentroidHomClass.map_mul_left` `instCentroidHomClass` `CentroidHomClass.map_mul_right` `Subsemiring.mem_centralizer_iff`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instAdd` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `comp`	—	—
`coe_comp_addMonoidHom` 📖	mathematical	—	`AddMonoidHomClass.toAddMonoidHom` `CentroidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass` `comp` `AddMonoidHom.comp`	—	`CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass`
`coe_copy` 📖	mathematical	`DFunLike.coe` `CentroidHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `id`	—	—
`coe_intCast` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instFunLike` `instIntCast` `SubNegMonoid.toZSMul` `Pi.subNegMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `id`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instMul`	—	—
`coe_natCast` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instNatCast` `AddMonoid.toNatSMul` `Pi.addMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `id`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instFunLike` `instNeg` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instOne`	—	—
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instSMul` `Function.hasSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instFunLike` `instSub` `Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`coe_toAddMonoidHom` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.instFunLike` `AddMonoidHomClass.toAddMonoidHom` `CentroidHom` `instFunLike` `CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass`	—	`CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass`
`coe_toAddMonoidHom_injective` 📖	mathematical	—	`CentroidHom` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHomClass.toAddMonoidHom` `instFunLike` `CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass`	—	`CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass` `ext` `DFunLike.congr_fun`
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instZero` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	—
`comp_mul_comm` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`CentroidHomClass.map_mul_right` `instCentroidHomClass` `CentroidHomClass.map_mul_left`
`copy_eq` 📖	mathematical	`DFunLike.coe` `CentroidHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `CentroidHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike`	—	`ext`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `id`	—	—
`id_comp` 📖	mathematical	—	`comp` `id`	—	—
`instCentroidHomClass` 📖	mathematical	—	`CentroidHomClass` `CentroidHom` `instFunLike`	—	`AddMonoidHom.map_add'` `ZeroHom.map_zero'` `map_mul_left'` `map_mul_right'`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `CentroidHom` `instSMul` `MulOpposite` `MulOpposite.instMonoid` `SMulCommClass.op_left` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NonUnitalNonAssocSemiring.toDistribSMul` `IsScalarTower.op_left`	—	`SMulCommClass.op_left` `IsScalarTower.op_left` `ext` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `CentroidHom` `instSMul`	—	`ext` `smul_assoc`
`instIsScalarTower_1` 📖	mathematical	—	`IsScalarTower` `CentroidHom` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `applyModule` `NonUnitalNonAssocSemiring.toDistribSMul`	—	`CentroidHomClass.map_mul_right` `instCentroidHomClass`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `CentroidHom` `instSMul`	—	`ext` `SMulCommClass.smul_comm`
`instSMulCommClass_1` 📖	mathematical	—	`SMulCommClass` `CentroidHom` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `applyModule` `NonUnitalNonAssocSemiring.toDistribSMul`	—	`CentroidHomClass.map_mul_left` `instCentroidHomClass`
`instSMulCommClass_2` 📖	mathematical	—	`SMulCommClass` `CentroidHom` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `NonUnitalNonAssocSemiring.toDistribSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `applyModule`	—	`SMulCommClass.symm` `instSMulCommClass_1`
`intCast_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instFunLike` `instIntCast` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`isScalarTowerRight` 📖	mathematical	—	`IsScalarTower` `CentroidHom` `instSMul` `instMul`	—	—
`map_mul_left'` 📖	mathematical	—	`ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.toZeroHom` `toAddMonoidHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`map_mul_right'` 📖	mathematical	—	`ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.toZeroHom` `toAddMonoidHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instMul`	—	—
`natCast_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instNatCast` `AddMonoid.toNatSMul` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instFunLike` `instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instOne`	—	—
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul`	—	—
`smul_def` 📖	mathematical	—	`CentroidHom` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Module.toDistribMulAction` `applyModule` `DFunLike.coe` `instFunLike`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instFunLike` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`toAddMonoidHom_eq_coe` 📖	mathematical	—	`toAddMonoidHom` `AddMonoidHomClass.toAddMonoidHom` `CentroidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass`	—	—
`toAddMonoidHom_id` 📖	mathematical	—	`AddMonoidHomClass.toAddMonoidHom` `CentroidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass` `id` `AddMonoidHom.id`	—	`CentroidHomClass.toAddMonoidHomClass` `instCentroidHomClass`
`toEndRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `CentroidHom` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toNonAssocSemiring` `instSemiring` `AddMonoid.End.instSemiring` `RingHom.instFunLike` `toEndRingHom` `toEnd`	—	—
`toEnd_add` 📖	mathematical	—	`toEnd` `CentroidHom` `instAdd` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoid.End.instSemiring`	—	—
`toEnd_injective` 📖	mathematical	—	`CentroidHom` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `toEnd`	—	`coe_toAddMonoidHom_injective`
`toEnd_intCast` 📖	mathematical	—	`toEnd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `CentroidHom` `instIntCast` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoid.End.instIntCast` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`toEnd_mul` 📖	mathematical	—	`toEnd` `CentroidHom` `instMul` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoid.End.instMul`	—	—
`toEnd_natCast` 📖	mathematical	—	`toEnd` `CentroidHom` `instNatCast` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toNatCast` `AddMonoid.End.instAddMonoidWithOne`	—	—
`toEnd_neg` 📖	mathematical	—	`toEnd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `CentroidHom` `instNeg` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoid.End.instAddCommGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`toEnd_one` 📖	mathematical	—	`toEnd` `CentroidHom` `instOne` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoid.End.instOne`	—	—
`toEnd_pow` 📖	mathematical	—	`toEnd` `CentroidHom` `hasNPowNat` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Monoid.toNatPow` `AddMonoid.End.instMonoid`	—	—
`toEnd_smul` 📖	mathematical	—	`toEnd` `CentroidHom` `instSMul` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddMonoidWithOne.toAddMonoid` `AddMonoid.End.instAddMonoidWithOne` `DistribSMul.toSMulZeroClass` `AddMonoid.End.instDistribSMul` `DistribMulAction.toDistribSMul`	—	—
`toEnd_sub` 📖	mathematical	—	`toEnd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `CentroidHom` `instSub` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoid.End.instRing` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`toEnd_zero` 📖	mathematical	—	`toEnd` `CentroidHom` `instZero` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoid.End.instSemiring`	—	—
`toFun_eq_coe` 📖	mathematical	—	`ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidHom.toZeroHom` `toAddMonoidHom` `DFunLike.coe` `CentroidHom` `instFunLike`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—

CentroidHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_mul_left` 📖	mathematical	—	`DFunLike.coe` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`map_mul_right` 📖	mathematical	—	`DFunLike.coe` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`toAddMonoidHomClass` 📖	mathematical	—	`AddMonoidHomClass` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	—

Module

Definitions

Name	Category	Theorems
`toCentroidHom` 📖	CompOp	1 math math: `toCentroidHom_apply_toFun`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCentroidHom_apply_toFun` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `CentroidHom.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CentroidHom.instSemiring` `RingHom.instFunLike` `toCentroidHom` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `toDistribMulAction`	—	—

NonUnitalNonAssocCommSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_center_iff` 📖	mathematical	—	`NonUnitalSubsemiring` `toNonUnitalNonAssocSemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `NonUnitalSubsemiring.center` `Commute` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoid.End.instMul` `DFunLike.coe` `AddMonoidHom` `AddMonoid.End.instAddCommMonoid` `AddMonoidHom.instFunLike` `AddMonoid.End.mulLeft`	—	`NonUnitalNonAssocSemiring.mem_center_iff` `CentroidHom.centroid_eq_centralizer_mulLeftRight` `Subsemiring.mem_centralizer_iff` `AddMonoid.End.mulRight_eq_mulLeft` `Set.union_self`

NonUnitalNonAssocSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_center_iff` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `NonUnitalSubsemiring.center` `DFunLike.coe` `AddMonoidHom` `AddMonoid.End` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `toAddCommMonoid` `AddMonoid.End.instAddCommMonoid` `AddMonoidHom.instFunLike` `AddMonoid.End.mulRight` `AddMonoid.End.mulLeft` `Subsemiring` `Semiring.toNonAssocSemiring` `AddMonoid.End.instSemiring` `Subsemiring.instSetLike` `RingHom.rangeS` `CentroidHom` `CentroidHom.instSemiring` `CentroidHom.toEndRingHom`	—	`AddMonoidHom.ext` `Commute.symm` `IsMulCentral.comm` `CentroidHomClass.map_mul_right` `CentroidHom.instCentroidHomClass` `CentroidHomClass.map_mul_left`

(root)

Definitions

Name	Category	Theorems
`CentroidHomClass` 📖	CompData	1 math math: `CentroidHom.instCentroidHomClass`
`instCoeTCCentroidHomOfCentroidHomClass` 📖	CompOp	—

---

← Back to Index