Documentation Verification Report

NonUnitalSubsemiring

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

Statistics

Metric	Count
Definitions `NonUnitalStarSubsemiring`, `center`, `copy`, `instSetLike`, `ofClass`, `toNonUnitalSubsemiring`, `NonUnitalSubsemiring`, `SubStarSemigroup`, `toSubsemigroup`	9
Theorems `coe_copy`, `coe_ofClass`, `copy_eq`, `instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar`, `instNonUnitalSubsemiringClass`, `instStarMemClass`, `mem_carrier`, `star_mem'`, `star_mem'`	9
Total	18

NonUnitalStarSubsemiring

Definitions

Name	Category	Theorems
`center` 📖	CompOp	3 math math: `CentroidHom.star_centerToCentroidCenter`, `CentroidHom.starCenterIsoCentroid_apply`, `CentroidHom.starCenterToCentroid_apply`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`instSetLike` 📖	CompOp	8 math math: `instNonUnitalSubsemiringClass`, `CentroidHom.star_centerToCentroidCenter`, `CentroidHom.starCenterIsoCentroid_apply`, `coe_ofClass`, `instStarMemClass`, `instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar`, `mem_carrier`, `CentroidHom.starCenterToCentroid_apply`
`ofClass` 📖	CompOp	1 math math: `coe_ofClass`
`toNonUnitalSubsemiring` 📖	CompOp	1 math math: `mem_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_copy` 📖	mathematical	`SetLike.coe` `NonUnitalStarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `instSetLike`	`copy`	—	—
`coe_ofClass` 📖	mathematical	—	`SetLike.coe` `NonUnitalStarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `instSetLike` `ofClass`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `NonUnitalStarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar` 📖	mathematical	—	`CanLift` `Set` `NonUnitalStarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `SetLike.coe` `instSetLike` `Set.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`instNonUnitalSubsemiringClass` 📖	mathematical	—	`NonUnitalSubsemiringClass` `NonUnitalStarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `instSetLike`	—	`AddSubsemigroup.add_mem'` `AddSubmonoid.zero_mem'` `NonUnitalSubsemiring.mul_mem'`
`instStarMemClass` 📖	mathematical	—	`StarMemClass` `NonUnitalStarSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `instSetLike`	—	`star_mem'`
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `toNonUnitalSubsemiring` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `StarRing.toStarAddMonoid` `NonUnitalStarSubsemiring` `SetLike.instMembership` `instSetLike`	—	—
`star_mem'` 📖	mathematical	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `toNonUnitalSubsemiring`	`Star.star`	—	—

SubStarSemigroup

Definitions

Name	Category	Theorems
`toSubsemigroup` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`star_mem'` 📖	mathematical	`Set` `Set.instMembership` `Subsemigroup.carrier` `toSubsemigroup`	`Star.star`	—	—

(root)

Definitions

Name	Category	Theorems
`NonUnitalStarSubsemiring` 📖	CompData	8 math math: `NonUnitalStarSubsemiring.instNonUnitalSubsemiringClass`, `CentroidHom.star_centerToCentroidCenter`, `CentroidHom.starCenterIsoCentroid_apply`, `NonUnitalStarSubsemiring.coe_ofClass`, `NonUnitalStarSubsemiring.instStarMemClass`, `NonUnitalStarSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallStar`, `NonUnitalStarSubsemiring.mem_carrier`, `CentroidHom.starCenterToCentroid_apply`
`NonUnitalSubsemiring` 📖	CompData	142 math math: `Subsemiring.mem_toNonUnitalSubsemiring`, `NonUnitalSubring.toNonUnitalSubsemiring_eq_top`, `NonUnitalSubsemiring.mem_bot`, `NonUnitalSubsemiring.srange_subtype`, `CentroidHom.star_centerToCentroidCenter`, `NonUnitalRingHom.srange_eq_map`, `NonUnitalSubsemiring.top_prod`, `NonUnitalSubring.toNonUnitalSubsemiring_strictMono`, `NonUnitalSubsemiring.isClosed_topologicalClosure`, `NonUnitalSubsemiring.coe_map`, `NonUnitalSubsemiring.coe_equivMapOfInjective_apply`, `NonUnitalSubsemiring.mem_map_equiv`, `NonUnitalSubsemiring.toAddSubmonoid_top`, `NonUnitalAlgebra.sInf_toNonUnitalSubsemiring`, `NonUnitalSubsemiring.centerCongr_symm_apply_coe`, `NonUnitalSubsemiring.mem_closure_of_mem`, `NonUnitalSubsemiring.subset_closure`, `NonUnitalSubsemiring.mem_top`, `NonUnitalSubsemiring.toAddSubmonoid_strictMono`, `NonUnitalRingHom.mem_srange`, `NonUnitalRingHom.mem_srange_self`, `NonUnitalSubsemiring.closure_union`, `NonUnitalSubalgebra.coe_toNonUnitalSubsemiring`, `NonUnitalSubsemiring.closure_empty`, `NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe`, `NonUnitalSubsemiring.mem_iInf`, `NonUnitalSubsemiring.center_eq_top`, `NonUnitalSubsemiring.coe_mk'`, `NonUnitalSubalgebra.mem_toNonUnitalSubsemiring`, `NonUnitalSubsemiring.comap_iInf`, `NonUnitalSubsemiring.gc_map_comap`, `NonUnitalSubsemiring.coe_add`, `RingEquiv.sofLeftInverse'_apply`, `NonUnitalSubsemiring.closure_le_centralizer_centralizer`, `NonUnitalSubsemiring.eq_top_iff'`, `NonUnitalSubsemiring.map_iInf`, `NonUnitalSubsemiring.coe_center`, `NonUnitalSubsemiring.closure_mono`, `NonUnitalSubsemiring.mem_sumSq`, `NonUnitalSubsemiring.coe_bot`, `NonUnitalSubsemiring.toSubsemigroup_strictMono`, `NonUnitalSubring.range_snd`, `NonUnitalSubsemiring.mem_sInf`, `NonUnitalSubsemiring.le_topologicalClosure`, `NonUnitalSubsemiring.toAddSubmonoid_eq_top`, `NonUnitalAlgebra.top_toNonUnitalSubsemiring`, `NonUnitalSubsemiring.toAddSubmonoid_mono`, `Subsemigroup.nonUnitalSubsemiringClosure_coe`, `NonUnitalSubsemiring.ext_iff`, `NonUnitalRingHom.srangeRestrict_surjective`, `NonUnitalSubsemiring.instNonUnitalSubsemiringClass`, `NonUnitalNonAssocCommSemiring.mem_center_iff`, `NonUnitalRingHom.sclosure_preimage_le`, `NonUnitalSubsemiring.map_iSup`, `NonUnitalSubring.mk_le_mk`, `NonUnitalRingHom.srange_eq_top_iff_surjective`, `NonUnitalSubring.mem_carrier`, `NonUnitalSubsemiring.map_le_iff_le_comap`, `NonUnitalSubsemiring.closure_univ`, `NonUnitalSubsemiring.prod_mono_left`, `NonUnitalSubring.toNonUnitalSubsemiring_top`, `NonUnitalSubsemiring.mem_center_iff`, `NonUnitalSubsemiring.coe_toSubsemigroup`, `NonUnitalSubsemiring.sInf_toAddSubmonoid`, `NonUnitalSubsemiring.mem_inf`, `NonUnitalSubsemiring.mem_mk'`, `NonUnitalSubsemiring.coe_sumSq`, `Subsemiring.coe_toNonUnitalSubsemiring`, `NonUnitalSubsemiring.toSubsemigroup_mono`, `NonUnitalSubsemiring.coe_iInf`, `NonUnitalSubsemiring.mem_map`, `NonUnitalSubring.mem_mk`, `NonUnitalSubsemiring.range_fst`, `NonUnitalSubsemiring.mem_carrier`, `Subsemiring.toNonUnitalSubsemiring_injective`, `NonUnitalSubsemiring.closure_sUnion`, `NonUnitalSubsemiring.closure_iUnion`, `NonUnitalSubsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul`, `RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe`, `NonUnitalSubsemiring.coe_toAddSubmonoid`, `NonUnitalRingHom.srange_eq_top_of_surjective`, `NonUnitalSubsemiring.coe_centralizer`, `NonUnitalSubsemiring.top_prod_top`, `NonUnitalNonAssocSemiring.mem_center_iff`, `Subsemiring.one_mem_toNonUnitalSubsemiring`, `NonUnitalSubalgebra.toNonUnitalSubsemiring_injective`, `NonUnitalSubsemiring.instIsTopologicalSemiring`, `NonUnitalSubsemiring.coe_prod`, `NonUnitalSubring.coe_set_mk`, `NonUnitalSubsemiring.toSubsemigroup_injective`, `NonUnitalSubsemiring.centralizer_eq_top_iff_subset`, `NonUnitalSubsemiring.closure_le`, `NonUnitalSubsemiring.centerToMulOpposite_apply_coe`, `RingEquiv.sofLeftInverse'_symm_apply`, `NonUnitalSubsemiring.coe_inf`, `NonUnitalSubsemiring.mem_closure`, `NonUnitalRingHom.finite_srange`, `NonUnitalSubsemiring.comap_inf`, `NonUnitalSubring.mem_toNonUnitalSubsemiring`, `CentroidHom.centerToCentroidCenter_apply`, `NonUnitalSubsemiring.center_le_centralizer`, `NonUnitalRingHom.coe_srange`, `NonUnitalSubsemiring.comap_top`, `NonUnitalSubsemiring.coe_mul`, `NonUnitalSubsemiring.mem_comap`, `NonUnitalSubsemiring.sInf_toSubsemigroup`, `NonUnitalSubsemiring.map_sup`, `NonUnitalSubsemiring.map_inf`, `NonUnitalSubsemiring.prod_top`, `NonUnitalSubsemiring.prod_mono_right`, `mem_nonUnitalSubalgebraOfNonUnitalSubsemiring`, `NonUnitalSubsemiring.coe_sInf`, `NonUnitalSubsemiring.toAddSubmonoid_injective`, `CentroidHom.centerToCentroid_apply`, `NonUnitalSubsemiring.coe_zero`, `NonUnitalSubring.coe_toNonUnitalSubsemiring`, `NonUnitalAlgebra.adjoin_toSubmodule`, `NonUnitalSubsemiring.mem_prod`, `NonUnitalRingHom.coe_srangeRestrict`, `NonUnitalSubsemiring.centerCongr_apply_coe`, `NonUnitalSubsemiring.ofClass_carrier`, `NonUnitalSubsemiring.map_bot`, `NonUnitalSubsemiring.mem_closure_iff`, `NonUnitalSubsemiring.coe_top`, `NonUnitalSubsemiring.mem_toSubsemigroup`, `RingEquiv.nonUnitalSubsemiringMap_apply_coe`, `NonUnitalSubsemiring.coe_closure_eq`, `NonUnitalSubsemiring.range_snd`, `NonUnitalAlgebra.inf_toNonUnitalSubsemiring`, `NonUnitalSubsemiring.topologicalClosure_coe`, `NonUnitalSubsemiring.mem_toAddSubmonoid`, `NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top`, `NonUnitalSubring.toNonUnitalSubsemiring_mono`, `NonUnitalSubring.toNonUnitalSubsemiring_injective`, `NonUnitalSubring.range_fst`, `NonUnitalSubsemiring.centralizer_le`, `NonUnitalSubsemiring.closure_eq`, `NonUnitalSubsemiring.topEquiv_symm_apply_coe`, `NonUnitalRingHom.eqOn_sclosure`, `NonUnitalSubsemiring.mem_centralizer_iff`, `NonUnitalSubsemiring.topEquiv_apply`, `NonUnitalSubsemiring.coe_comap`
`SubStarSemigroup` 📖	CompData	—

---

← Back to Index