Documentation Verification Report

CentroidHom

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

Statistics

Metric	Count
Definitions `CentroidHom`, `centerStarEmbedding`, `instStar`, `instStarAddMonoid`, `instStarAddMonoidCenter`, `instStarRingSubtypeMemSubsemiringCenter`, `instStarSubtypeMemSubsemiringCenter`, `starCenterIsoCentroid`, `starCenterToCentroid`, `starCenterToCentroidCenter`, `starRingOfCommCentroidHom`	11
Theorems `starCenterIsoCentroid_apply`, `starCenterIsoCentroid_symm_apply_coe`, `starCenterToCentroid_apply`, `star_apply`, `star_centerToCentroidCenter`	5
Total	16

CentroidHom

Definitions

Name	Category	Theorems
`centerStarEmbedding` 📖	CompOp	—
`instStar` 📖	CompOp	4 math math: `starCenterIsoCentroid_symm_apply_coe`, `starCenterIsoCentroid_apply`, `star_apply`, `starCenterToCentroid_apply`
`instStarAddMonoid` 📖	CompOp	—
`instStarAddMonoidCenter` 📖	CompOp	—
`instStarRingSubtypeMemSubsemiringCenter` 📖	CompOp	—
`instStarSubtypeMemSubsemiringCenter` 📖	CompOp	1 math math: `star_centerToCentroidCenter`
`starCenterIsoCentroid` 📖	CompOp	2 math math: `starCenterIsoCentroid_symm_apply_coe`, `starCenterIsoCentroid_apply`
`starCenterToCentroid` 📖	CompOp	2 math math: `starCenterIsoCentroid_apply`, `starCenterToCentroid_apply`
`starCenterToCentroidCenter` 📖	CompOp	—
`starRingOfCommCentroidHom` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`starCenterIsoCentroid_apply` 📖	mathematical	—	`DFunLike.coe` `StarRingEquiv` `StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `SetLike.instMembership` `StarSubsemiring.setLike` `StarSubsemiring.center` `CentroidHom` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `StarSubsemiring.semiring` `instAdd` `Distrib.toMul` `instMul` `StarMemClass.instStar` `StarSubsemiring.starMemClass` `instStar` `StarRingEquiv.instFunLike` `starCenterIsoCentroid` `NonUnitalStarRingHom` `NonUnitalStarSubsemiring` `NonUnitalStarSubsemiring.instSetLike` `NonUnitalStarSubsemiring.center` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `NonUnitalStarSubsemiring.instNonUnitalSubsemiringClass` `NonUnitalStarSubsemiring.instStarMemClass` `Semiring.toNonAssocSemiring` `instSemiring` `NonUnitalStarRingHom.instFunLike` `starCenterToCentroid`	—	`StarSubsemiring.starMemClass`
`starCenterIsoCentroid_symm_apply_coe` 📖	mathematical	—	`StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `SetLike.instMembership` `StarSubsemiring.setLike` `StarSubsemiring.center` `DFunLike.coe` `StarRingEquiv` `CentroidHom` `instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `StarSubsemiring.semiring` `instMul` `Distrib.toMul` `instStar` `StarMemClass.instStar` `StarSubsemiring.starMemClass` `StarRingEquiv.instFunLike` `StarRingEquiv.symm` `starCenterIsoCentroid` `instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`StarSubsemiring.starMemClass`
`starCenterToCentroid_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `NonUnitalStarRingHom` `NonUnitalStarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SetLike.instMembership` `NonUnitalStarSubsemiring.instSetLike` `NonUnitalStarSubsemiring.center` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `NonUnitalStarSubsemiring.instNonUnitalSubsemiringClass` `StarMemClass.instStar` `NonUnitalStarSubsemiring.instStarMemClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiring` `instStar` `NonUnitalStarRingHom.instFunLike` `starCenterToCentroid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`NonUnitalStarSubsemiring.instNonUnitalSubsemiringClass` `NonUnitalStarSubsemiring.instStarMemClass`
`star_apply` 📖	mathematical	—	`DFunLike.coe` `CentroidHom` `instFunLike` `Star.star` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid`	—	—
`star_centerToCentroidCenter` 📖	mathematical	—	`Star.star` `CentroidHom` `Subsemiring` `Semiring.toNonAssocSemiring` `instSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `Subsemiring.center` `instStarSubtypeMemSubsemiringCenter` `DFunLike.coe` `NonUnitalRingHom` `NonUnitalSubsemiring` `NonUnitalSubsemiring.instSetLike` `NonUnitalSubsemiring.center` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalSubsemiring.center.instNonUnitalCommSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Subsemiring.toNonAssocSemiring` `NonUnitalRingHom.instFunLike` `centerToCentroidCenter` `NonUnitalStarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `NonUnitalStarSubsemiring.instSetLike` `NonUnitalStarSubsemiring.center` `StarMemClass.instStar` `NonUnitalStarSubsemiring.instStarMemClass`	—	`NonUnitalStarSubsemiring.instStarMemClass` `ext` `StarMul.star_mul` `star_star` `IsMulCentral.comm`

(root)

Definitions

Name	Category	Theorems
`CentroidHom` 📖	CompData	61 math math: `CentroidHom.toEnd_pow`, `CentroidHom.toEnd_sub`, `CentroidHom.toEnd_one`, `CentroidHom.star_centerToCentroidCenter`, `CentroidHom.starCenterIsoCentroid_symm_apply_coe`, `CentroidHom.zero_apply`, `CentroidHom.coe_toAddMonoidHom`, `CentroidHom.natCast_apply`, `CentroidHom.starCenterIsoCentroid_apply`, `CentroidHom.smul_def`, `CentroidHom.coe_add`, `CentroidHom.centroid_eq_centralizer_mulLeftRight`, `CentroidHom.instSMulCommClass_2`, `CentroidHom.toEnd_smul`, `CentroidHom.toEnd_add`, `CentroidHom.neg_apply`, `CentroidHom.sub_apply`, `CentroidHom.star_apply`, `CentroidHom.smul_apply`, `CentroidHom.toEnd_intCast`, `CentroidHom.toAddMonoidHom_id`, `CentroidHom.coe_intCast`, `CentroidHom.coe_sub`, `CentroidHom.coe_one`, `CentroidHom.coe_neg`, `CentroidHom.coe_id`, `Module.toCentroidHom_apply_toFun`, `CentroidHom.instIsScalarTower`, `CentroidHom.ext_iff`, `CentroidHom.comp_apply`, `CentroidHom.add_apply`, `CentroidHom.id_apply`, `CentroidHom.coe_comp`, `CentroidHom.instCentroidHomClass`, `CentroidHom.instSMulCommClass_1`, `CentroidHom.instIsScalarTower_1`, `CentroidHom.coe_toAddMonoidHom_injective`, `CentroidHom.toEnd_natCast`, `CentroidHom.toEnd_zero`, `CentroidHom.instSMulCommClass`, `CentroidHom.toFun_eq_coe`, `CentroidHom.comp_mul_comm`, `CentroidHom.toEndRingHom_apply`, `CentroidHom.coe_zero`, `CentroidHom.toEnd_injective`, `CentroidHom.mul_apply`, `CentroidHom.toEnd_mul`, `CentroidHom.toAddMonoidHom_eq_coe`, `NonUnitalNonAssocSemiring.mem_center_iff`, `CentroidHom.instIsCentralScalar`, `CentroidHom.toEnd_neg`, `CentroidHom.coe_comp_addMonoidHom`, `CentroidHom.centerToCentroidCenter_apply`, `CentroidHom.coe_smul`, `CentroidHom.centerToCentroid_apply`, `CentroidHom.starCenterToCentroid_apply`, `CentroidHom.intCast_apply`, `CentroidHom.one_apply`, `CentroidHom.coe_natCast`, `CentroidHom.isScalarTowerRight`, `CentroidHom.coe_mul`

---

← Back to Index