Defs

📁 Source: Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean

Statistics

Metric	Count
Definitions `codRestrict`, `eqSlocus`, `copy`, `inclusion`, `instBot`, `instInhabited`, `instMin`, `instPartialOrder`, `instSetLike`, `instTop`, `mk'`, `ofClass`, `toAddSubmonoid`, `toSubsemigroup`, `NonUnitalSubsemiringClass`, `subtype`, `toNonUnitalCommSemiring`, `toNonUnitalNonAssocSemiring`, `toNonUnitalSemiring`	19
Theorems `coe_add`, `coe_bot`, `coe_copy`, `coe_inf`, `coe_mk'`, `coe_mul`, `coe_toAddSubmonoid`, `coe_toSubsemigroup`, `coe_top`, `coe_zero`, `copy_eq`, `ext`, `ext_iff`, `instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul`, `instNonUnitalSubsemiringClass`, `mem_bot`, `mem_carrier`, `mem_inf`, `mem_mk'`, `mem_toAddSubmonoid`, `mem_toSubsemigroup`, `mem_top`, `mk'_toAddSubmonoid`, `mk'_toSubsemigroup`, `mul_mem'`, `ofClass_carrier`, `toAddSubmonoid_eq_top`, `toAddSubmonoid_inj`, `toAddSubmonoid_injective`, `toAddSubmonoid_top`, `toSubsemigroup_injective`, `coe_subtype`, `mulMemClass`, `mul_mem`, `noZeroDivisors`, `subtype_apply`, `subtype_injective`, `toAddSubmonoidClass`, `mul_neg_mem`, `neg_mul_mem`	40
Total	59

NonUnitalRingHom

Definitions

Name	Category	Theorems
`codRestrict` 📖	CompOp	—
`eqSlocus` 📖	CompOp	—

NonUnitalSubsemiring

Definitions

Name	Category	Theorems
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`inclusion` 📖	CompOp	—
`instBot` 📖	CompOp	4 math math: `mem_bot`, `closure_empty`, `coe_bot`, `map_bot`
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	5 math math: `mem_inf`, `coe_inf`, `comap_inf`, `map_inf`, `NonUnitalAlgebra.inf_toNonUnitalSubsemiring`
`instPartialOrder` 📖	CompOp	18 math math: `NonUnitalSubring.toNonUnitalSubsemiring_strictMono`, `toAddSubmonoid_strictMono`, `gc_map_comap`, `closure_le_centralizer_centralizer`, `closure_mono`, `toSubsemigroup_strictMono`, `le_topologicalClosure`, `toAddSubmonoid_mono`, `NonUnitalRingHom.sclosure_preimage_le`, `NonUnitalSubring.mk_le_mk`, `map_le_iff_le_comap`, `prod_mono_left`, `toSubsemigroup_mono`, `closure_le`, `center_le_centralizer`, `prod_mono_right`, `NonUnitalSubring.toNonUnitalSubsemiring_mono`, `centralizer_le`
`instSetLike` 📖	CompOp	91 math math: `Subsemiring.mem_toNonUnitalSubsemiring`, `mem_bot`, `mem_iSup_of_directed`, `srange_subtype`, `CentroidHom.star_centerToCentroidCenter`, `isClosed_topologicalClosure`, `coe_map`, `coe_equivMapOfInjective_apply`, `mem_map_equiv`, `centerCongr_symm_apply_coe`, `mem_closure_of_mem`, `subset_closure`, `mem_top`, `NonUnitalRingHom.mem_srange`, `NonUnitalRingHom.mem_srange_self`, `NonUnitalSubalgebra.coe_toNonUnitalSubsemiring`, `centerToMulOpposite_symm_apply_coe`, `mem_iInf`, `coe_mk'`, `NonUnitalSubalgebra.mem_toNonUnitalSubsemiring`, `coe_iSup_of_directed`, `coe_add`, `RingEquiv.sofLeftInverse'_apply`, `closure_le_centralizer_centralizer`, `eq_top_iff'`, `coe_center`, `mem_sumSq`, `coe_bot`, `mem_sInf`, `Subsemigroup.nonUnitalSubsemiringClosure_coe`, `ext_iff`, `NonUnitalRingHom.srangeRestrict_surjective`, `instNonUnitalSubsemiringClass`, `NonUnitalNonAssocCommSemiring.mem_center_iff`, `NonUnitalSubring.mem_carrier`, `mem_center_iff`, `coe_toSubsemigroup`, `mem_inf`, `mem_mk'`, `coe_sumSq`, `Subsemiring.coe_toNonUnitalSubsemiring`, `coe_iInf`, `mem_map`, `NonUnitalSubring.mem_mk`, `mem_carrier`, `instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul`, `RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe`, `coe_toAddSubmonoid`, `coe_centralizer`, `NonUnitalNonAssocSemiring.mem_center_iff`, `Subsemiring.one_mem_toNonUnitalSubsemiring`, `instIsTopologicalSemiring`, `coe_prod`, `NonUnitalSubring.coe_set_mk`, `centralizer_eq_top_iff_subset`, `closure_le`, `centerToMulOpposite_apply_coe`, `RingEquiv.sofLeftInverse'_symm_apply`, `coe_inf`, `mem_closure`, `NonUnitalRingHom.finite_srange`, `NonUnitalSubring.mem_toNonUnitalSubsemiring`, `CentroidHom.centerToCentroidCenter_apply`, `NonUnitalRingHom.coe_srange`, `coe_mul`, `mem_comap`, `mem_nonUnitalSubalgebraOfNonUnitalSubsemiring`, `coe_sInf`, `CentroidHom.centerToCentroid_apply`, `coe_zero`, `NonUnitalSubring.coe_toNonUnitalSubsemiring`, `NonUnitalAlgebra.adjoin_toSubmodule`, `mem_prod`, `NonUnitalRingHom.coe_srangeRestrict`, `centerCongr_apply_coe`, `coe_sSup_of_directedOn`, `ofClass_carrier`, `mem_sSup_of_directedOn`, `mem_closure_iff`, `coe_top`, `mem_toSubsemigroup`, `RingEquiv.nonUnitalSubsemiringMap_apply_coe`, `coe_closure_eq`, `topologicalClosure_coe`, `mem_toAddSubmonoid`, `closure_eq`, `topEquiv_symm_apply_coe`, `NonUnitalRingHom.eqOn_sclosure`, `mem_centralizer_iff`, `topEquiv_apply`, `coe_comap`
`instTop` 📖	CompOp	25 math math: `NonUnitalSubring.toNonUnitalSubsemiring_eq_top`, `NonUnitalRingHom.srange_eq_map`, `top_prod`, `toAddSubmonoid_top`, `mem_top`, `center_eq_top`, `eq_top_iff'`, `NonUnitalSubring.range_snd`, `toAddSubmonoid_eq_top`, `NonUnitalAlgebra.top_toNonUnitalSubsemiring`, `NonUnitalRingHom.srange_eq_top_iff_surjective`, `closure_univ`, `NonUnitalSubring.toNonUnitalSubsemiring_top`, `range_fst`, `NonUnitalRingHom.srange_eq_top_of_surjective`, `top_prod_top`, `centralizer_eq_top_iff_subset`, `comap_top`, `prod_top`, `coe_top`, `range_snd`, `NonUnitalAlgebra.toNonUnitalSubsemiring_eq_top`, `NonUnitalSubring.range_fst`, `topEquiv_symm_apply_coe`, `topEquiv_apply`
`mk'` 📖	CompOp	4 math math: `mk'_toAddSubmonoid`, `mk'_toSubsemigroup`, `coe_mk'`, `mem_mk'`
`ofClass` 📖	CompOp	1 math math: `ofClass_carrier`
`toAddSubmonoid` 📖	CompOp	21 math math: `NonUnitalStarSubalgebra.mem_carrier`, `mk'_toAddSubmonoid`, `Subalgebra.coe_center`, `sumSq_toAddSubmonoid`, `toAddSubmonoid_top`, `toAddSubmonoid_strictMono`, `toAddSubmonoid_inj`, `toAddSubmonoid_eq_top`, `toAddSubmonoid_mono`, `Subsemiring.center_toSubmonoid`, `NonUnitalStarSubsemiring.mem_carrier`, `sInf_toAddSubmonoid`, `mem_carrier`, `RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe`, `NonUnitalSubalgebra.mem_carrier`, `coe_toAddSubmonoid`, `toAddSubmonoid_injective`, `Subsemiring.coe_center`, `RingEquiv.nonUnitalSubsemiringMap_apply_coe`, `Subsemigroup.nonUnitalSubsemiringClosure_toAddSubmonoid`, `mem_toAddSubmonoid`
`toSubsemigroup` 📖	CompOp	9 math math: `mk'_toSubsemigroup`, `toSubsemigroup_strictMono`, `coe_toSubsemigroup`, `toSubsemigroup_mono`, `toSubsemigroup_injective`, `centralizer_toSubsemigroup`, `sInf_toSubsemigroup`, `center_toSubsemigroup`, `mem_toSubsemigroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_add` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `instNonUnitalSubsemiringClass`	—	`instNonUnitalSubsemiringClass`
`coe_bot` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`coe_copy` 📖	mathematical	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike`	`copy`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_mk'` 📖	mathematical	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instSetLike` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike`	`NonUnitalSubsemiring` `instSetLike` `mk'`	—	—
`coe_mul` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring` `instNonUnitalSubsemiringClass`	—	`instNonUnitalSubsemiringClass`
`coe_toAddSubmonoid` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike` `toAddSubmonoid` `NonUnitalSubsemiring` `instSetLike`	—	—
`coe_toSubsemigroup` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instSetLike` `toSubsemigroup` `NonUnitalSubsemiring` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`coe_zero` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `instNonUnitalSubsemiringClass`	—	`AddSubmonoidClass.toZeroMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `instNonUnitalSubsemiringClass`
`copy_eq` 📖	mathematical	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`ext` 📖	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike`	—	`ext`
`instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul` 📖	mathematical	—	`CanLift` `Set` `NonUnitalSubsemiring` `SetLike.coe` `instSetLike` `Set.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`instNonUnitalSubsemiringClass` 📖	mathematical	—	`NonUnitalSubsemiringClass` `NonUnitalSubsemiring` `instSetLike`	—	`AddSubsemigroup.add_mem'` `AddSubmonoid.zero_mem'` `mul_mem'`
`mem_bot` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `Bot.bot` `instBot` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Set.mem_singleton_iff`
`mem_carrier` 📖	mathematical	—	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.toAddSubsemigroup` `toAddSubmonoid` `NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike`	—	—
`mem_inf` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `instMin`	—	—
`mem_mk'` 📖	mathematical	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instSetLike` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike`	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `mk'` `Set` `Set.instMembership`	—	—
`mem_toAddSubmonoid` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `SetLike.instMembership` `AddSubmonoid.instSetLike` `toAddSubmonoid` `NonUnitalSubsemiring` `instSetLike`	—	—
`mem_toSubsemigroup` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `SetLike.instMembership` `Subsemigroup.instSetLike` `toSubsemigroup` `NonUnitalSubsemiring` `instSetLike`	—	—
`mem_top` 📖	mathematical	—	`NonUnitalSubsemiring` `SetLike.instMembership` `instSetLike` `Top.top` `instTop`	—	`Set.mem_univ`
`mk'_toAddSubmonoid` 📖	mathematical	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instSetLike` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike`	`toAddSubmonoid` `mk'`	—	`SetLike.coe_injective`
`mk'_toSubsemigroup` 📖	mathematical	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Subsemigroup.instSetLike` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instSetLike`	`toSubsemigroup` `mk'`	—	`SetLike.coe_injective`
`mul_mem'` 📖	mathematical	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.toAddSubsemigroup` `toAddSubmonoid`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`ofClass_carrier` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `instSetLike` `ofClass`	—	—
`toAddSubmonoid_eq_top` 📖	mathematical	—	`toAddSubmonoid` `Top.top` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instTop` `NonUnitalSubsemiring` `instTop`	—	—
`toAddSubmonoid_inj` 📖	mathematical	—	`toAddSubmonoid`	—	`toAddSubmonoid_injective`
`toAddSubmonoid_injective` 📖	mathematical	—	`NonUnitalSubsemiring` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `toAddSubmonoid`	—	`mul_mem'`
`toAddSubmonoid_top` 📖	mathematical	—	`toAddSubmonoid` `Top.top` `NonUnitalSubsemiring` `instTop` `AddSubmonoid` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddSubmonoid.instTop`	—	—
`toSubsemigroup_injective` 📖	mathematical	—	`NonUnitalSubsemiring` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `toSubsemigroup`	—	`SetLike.ext` `SetLike.ext_iff`

NonUnitalSubsemiringClass

Definitions

Name	Category	Theorems
`subtype` 📖	CompOp	5 math math: `subtype_apply`, `NonUnitalSubsemiring.srange_subtype`, `coe_subtype`, `subtype_injective`, `NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype`
`toNonUnitalCommSemiring` 📖	CompOp	—
`toNonUnitalNonAssocSemiring` 📖	CompOp	41 math math: `NonUnitalStarAlgHom.coe_codRestrict`, `NonUnitalSubalgebraClass.coe_subtype`, `subtype_apply`, `NonUnitalSubsemiring.srange_subtype`, `NonUnitalSubsemiring.coe_equivMapOfInjective_apply`, `noZeroDivisors`, `CentroidHom.starCenterIsoCentroid_apply`, `NonUnitalStarAlgHom.injective_codRestrict`, `NonUnitalSubsemiring.coe_add`, `RingEquiv.sofLeftInverse'_apply`, `NonUnitalStarSubalgebra.instIsTorsionFree`, `NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype`, `NonUnitalSubalgebra.toSubring_subtype`, `NonUnitalStarSubalgebra.range_val`, `NonUnitalRingHom.srangeRestrict_surjective`, `NonUnitalSubalgebraClass.subtype_injective`, `coe_subtype`, `NonUnitalStarSubalgebraClass.coe_subtype`, `subtype_injective`, `RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe`, `NonUnitalStarSubalgebraClass.subtype_injective`, `NonUnitalStarSubalgebra.instSMulCommClass'`, `NonUnitalStarSubalgebra.toSubring_subtype`, `NonUnitalStarAlgHom.subtype_comp_codRestrict`, `NonUnitalStarSubalgebra.coe_mul`, `RingEquiv.sofLeftInverse'_symm_apply`, `NonUnitalSubalgebra.toNonUnitalSubsemiring_subtype`, `NonUnitalStarSubalgebra.coe_add`, `NonUnitalSubsemiring.coe_mul`, `NonUnitalStarSubalgebra.instIsScalarTower`, `NonUnitalSubalgebraClass.subtype_apply`, `CentroidHom.starCenterToCentroid_apply`, `NonUnitalRingHom.coe_srangeRestrict`, `RingEquiv.nonUnitalSubsemiringMap_apply_coe`, `NonUnitalStarSubalgebra.instSMulCommClass`, `NonUnitalStarSubalgebraClass.subtype_apply`, `NonUnitalStarSubalgebra.instIsScalarTower'`, `NonUnitalSubalgebra.range_val`, `NonUnitalAlgHom.subtype_comp_codRestrict`, `NonUnitalSubsemiring.topEquiv_symm_apply_coe`, `NonUnitalSubsemiring.topEquiv_apply`
`toNonUnitalSemiring` 📖	CompOp	12 math math: `NonUnitalSubalgebra.unitization_injective`, `NonUnitalStarSubalgebra.unitization_range`, `NonUnitalSubalgebra.unitization_range`, `NonUnitalSubsemiring.unitization_apply`, `NonUnitalSubring.unitization_apply`, `NonUnitalStarSubalgebra.unitization_injective`, `NonUnitalStarSubalgebra.unitization_apply`, `NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe`, `NonUnitalSubalgebra.unitization_apply`, `NonUnitalSubring.unitization_range`, `NonUnitalSubsemiring.instIsTopologicalSemiring`, `NonUnitalSubsemiring.unitization_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `NonUnitalRingHom` `SetLike.instMembership` `toNonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `subtype`	—	—
`mulMemClass` 📖	mathematical	—	`MulMemClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_mem`
`mul_mem` 📖	mathematical	`SetLike.instMembership`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	—
`noZeroDivisors` 📖	mathematical	—	`NoZeroDivisors` `SetLike.instMembership` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `toNonUnitalNonAssocSemiring` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `toAddSubmonoidClass`	—	`Function.Injective.noZeroDivisors` `AddSubmonoidClass.toZeroMemClass` `toAddSubmonoidClass` `Subtype.coe_injective`
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalRingHom` `SetLike.instMembership` `toNonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `NonUnitalRingHom` `toNonUnitalNonAssocSemiring` `NonUnitalRingHom.instFunLike` `subtype`	—	`Subtype.coe_injective`
`toAddSubmonoidClass` 📖	mathematical	—	`AddSubmonoidClass` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	—

(root)

Definitions

Name	Category	Theorems
`NonUnitalSubsemiringClass` 📖	CompData	7 math math: `NonUnitalStarSubsemiring.instNonUnitalSubsemiringClass`, `NonUnitalSubringClass.toNonUnitalSubsemiringClass`, `NonUnitalSubalgebra.instNonUnitalSubsemiringClass`, `instNonUnitalSubsemiringClassIdeal`, `NonUnitalSubsemiring.instNonUnitalSubsemiringClass`, `NonUnitalStarSubalgebra.instNonUnitalSubsemiringClass`, `SubsemiringClass.nonUnitalSubsemiringClass`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_neg_mem` 📖	—	`SetLike.instMembership` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	—	—	`mul_neg` `MulMemClass.mul_mem`
`neg_mul_mem` 📖	—	`SetLike.instMembership` `InvolutiveNeg.toNeg` `HasDistribNeg.toInvolutiveNeg`	—	—	`neg_mul` `MulMemClass.mul_mem`

---

← Back to Index