Documentation Verification Report

Subsemiring

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

Statistics

Metric	Count
Definitions `StarSubsemiring`, `center`, `copy`, `instPartialOrder`, `ofClass`, `semiring`, `setLike`, `starRing`, `toSubsemiring`, `center`	10
Theorems `coe_copy`, `coe_mk`, `coe_ofClass`, `coe_toSubsemiring`, `copy_eq`, `ext`, `ext_iff`, `instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar`, `mem_carrier`, `mem_toSubsemiring`, `starMemClass`, `star_mem'`, `subsemiringClass`, `toSubsemiring_inj`, `toSubsemiring_injective`, `toSubsemiring_le_iff`	16
Total	26

StarSubsemiring

Definitions

Name	Category	Theorems
`center` 📖	CompOp	2 math math: `CentroidHom.starCenterIsoCentroid_symm_apply_coe`, `CentroidHom.starCenterIsoCentroid_apply`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`instPartialOrder` 📖	CompOp	1 math math: `toSubsemiring_le_iff`
`ofClass` 📖	CompOp	1 math math: `coe_ofClass`
`semiring` 📖	CompOp	2 math math: `CentroidHom.starCenterIsoCentroid_symm_apply_coe`, `CentroidHom.starCenterIsoCentroid_apply`
`setLike` 📖	CompOp	11 math math: `CentroidHom.starCenterIsoCentroid_symm_apply_coe`, `mem_toSubsemiring`, `CentroidHom.starCenterIsoCentroid_apply`, `instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar`, `coe_toSubsemiring`, `subsemiringClass`, `mem_carrier`, `coe_mk`, `starMemClass`, `ext_iff`, `coe_ofClass`
`starRing` 📖	CompOp	—
`toSubsemiring` 📖	CompOp	6 math math: `mem_toSubsemiring`, `toSubsemiring_le_iff`, `toSubsemiring_injective`, `coe_toSubsemiring`, `mem_carrier`, `toSubsemiring_inj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_copy` 📖	mathematical	`SetLike.coe` `StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `setLike`	`copy`	—	—
`coe_mk` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `Star.star` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	`SetLike.coe` `StarSubsemiring` `setLike` `Subsemiring` `Subsemiring.instSetLike`	—	—
`coe_ofClass` 📖	mathematical	—	`SetLike.coe` `StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `setLike` `ofClass`	—	—
`coe_toSubsemiring` 📖	mathematical	—	`SetLike.coe` `Subsemiring` `Subsemiring.instSetLike` `toSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `StarSubsemiring` `setLike`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `setLike`	`copy`	—	`SetLike.coe_injective`
`ext` 📖	—	`StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `SetLike.instMembership` `setLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `SetLike.instMembership` `setLike`	—	`ext`
`instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar` 📖	mathematical	—	`CanLift` `Set` `StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `SetLike.coe` `setLike` `Set.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	—
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `toSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `StarSubsemiring` `SetLike.instMembership` `setLike`	—	—
`mem_toSubsemiring` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `toSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `StarSubsemiring` `setLike`	—	—
`starMemClass` 📖	mathematical	—	`StarMemClass` `StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `setLike`	—	`star_mem'`
`star_mem'` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `MulOne.toMul` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Submonoid.toSubsemigroup` `Subsemiring.toSubmonoid` `toSubsemiring`	`Star.star`	—	—
`subsemiringClass` 📖	mathematical	—	`SubsemiringClass` `StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `setLike`	—	`Subsemigroup.mul_mem'` `Submonoid.one_mem'` `Subsemiring.add_mem'` `Subsemiring.zero_mem'`
`toSubsemiring_inj` 📖	mathematical	—	`toSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid`	—	`toSubsemiring_injective`
`toSubsemiring_injective` 📖	mathematical	—	`StarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `Subsemiring` `toSubsemiring`	—	`ext` `mem_toSubsemiring`
`toSubsemiring_le_iff` 📖	mathematical	—	`Subsemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Subsemiring.instPartialOrder` `toSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `StarRing.toStarAddMonoid` `StarSubsemiring` `instPartialOrder`	—	—

SubStarSemigroup

Definitions

Name	Category	Theorems
`center` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`StarSubsemiring` 📖	CompData	13 math math: `CentroidHom.starCenterIsoCentroid_symm_apply_coe`, `StarSubsemiring.mem_toSubsemiring`, `CentroidHom.starCenterIsoCentroid_apply`, `StarSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar`, `StarSubsemiring.toSubsemiring_le_iff`, `StarSubsemiring.toSubsemiring_injective`, `StarSubsemiring.coe_toSubsemiring`, `StarSubsemiring.subsemiringClass`, `StarSubsemiring.mem_carrier`, `StarSubsemiring.coe_mk`, `StarSubsemiring.starMemClass`, `StarSubsemiring.ext_iff`, `StarSubsemiring.coe_ofClass`

---

← Back to Index