Defs

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

Statistics

Metric	Count
Definitions `NonUnitalSubring`, `copy`, `inclusion`, `instPartialOrder`, `instSetLike`, `mk'`, `ofClass`, `toAddSubgroup`, `toNonUnitalCommRing`, `toNonUnitalRing`, `toNonUnitalSubsemiring`, `toSubsemigroup`, `NonUnitalSubringClass`, `subtype`, `toNonUnitalCommRing`, `toNonUnitalNonAssocCommRing`, `toNonUnitalNonAssocRing`, `toNonUnitalRing`	18
Theorems `add_mem`, `coe_copy`, `coe_eq_zero_iff`, `coe_mk'`, `coe_set_mk`, `coe_toAddSubgroup`, `coe_toNonUnitalSubsemiring`, `coe_toSubsemigroup`, `copy_eq`, `ext`, `ext_iff`, `instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg`, `instNonUnitalSubringClass`, `mem_carrier`, `mem_mk`, `mem_mk'`, `mem_toAddSubgroup`, `mem_toNonUnitalSubsemiring`, `mem_toSubsemigroup`, `mk'_toAddSubgroup`, `mk'_toSubsemigroup`, `mk_le_mk`, `mul_mem`, `neg_mem`, `neg_mem'`, `ofClass_carrier`, `sub_mem`, `toAddSubgroup_injective`, `toAddSubgroup_mono`, `toAddSubgroup_strictMono`, `toNonUnitalSubsemiring_injective`, `toNonUnitalSubsemiring_mono`, `toNonUnitalSubsemiring_strictMono`, `toSubsemigroup_injective`, `toSubsemigroup_mono`, `toSubsemigroup_strictMono`, `val_add`, `val_mul`, `val_neg`, `val_zero`, `zero_mem`, `zsmul_mem`, `addSubgroupClass`, `coe_subtype`, `subtype_apply`, `subtype_injective`, `toNegMemClass`, `toNonUnitalSubsemiringClass`	48
Total	66

NonUnitalSubring

Definitions

Name	Category	Theorems
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`inclusion` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	24 math math: `toAddSubgroup_mono`, `toNonUnitalSubsemiring_strictMono`, `closure_preimage_le`, `topologicalClosure_minimal`, `centralizer_le`, `closure_mono`, `topologicalClosure_mono`, `ValuationSubring.nonunits_le_nonunits`, `map_le_iff_le_comap`, `prod_mono_left`, `mk_le_mk`, `prod_mono`, `toSubsemigroup_mono`, `ValuationSubring.nonunits_le`, `toAddSubgroup_strictMono`, `gc_map_comap`, `center_le_centralizer`, `prod_mono_right`, `toSubsemigroup_strictMono`, `NonUnitalRingHom.closure_preimage_le`, `closure_le_centralizer_centralizer`, `toNonUnitalSubsemiring_mono`, `le_topologicalClosure`, `closure_le`
`instSetLike` 📖	CompOp	100 math math: `instIsTopologicalRing`, `mem_closure_of_mem`, `coe_top`, `ValuationSubring.image_maximalIdeal`, `coe_sInf`, `NonUnitalRingHom.mem_range`, `mem_centralizer_iff`, `ext_iff`, `eq_top_iff'`, `ValuationSubring.nonunits_subset`, `NonUnitalSubalgebra.coe_toNonUnitalSubring`, `centerCongr_apply_coe`, `mem_sSup_of_directedOn`, `NonUnitalStarSubalgebra.coe_toNonUnitalSubring`, `zero_mem`, `mem_top`, `mem_inf`, `mem_center_iff`, `topEquiv_symm_apply_coe`, `NonUnitalRingHom.eqOn_set_closure`, `isMulCommutative_closure`, `neg_mem`, `coe_mk'`, `Ideal.image_subset_nonunits_valuationSubring`, `mem_iSup_of_directed`, `isClosed_topologicalClosure`, `NonUnitalRingHom.mem_range_self`, `topEquiv_apply`, `NonUnitalStarSubalgebra.mem_toNonUnitalSubring`, `ofClass_carrier`, `val_mul`, `closure_eq`, `coe_iInf`, `mem_toSubsemigroup`, `zsmul_mem`, `instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg`, `val_zero`, `centerCongr_symm_apply_coe`, `instNonUnitalSubringClass`, `coe_toAddSubgroup`, `val_neg`, `mem_bot`, `mem_carrier`, `coe_bot`, `mem_map`, `NonUnitalRingHom.coe_range`, `mul_mem`, `ValuationSubring.coe_mem_nonunits_iff`, `ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal`, `RingEquiv.ofLeftInverse'_symm_apply`, `mem_mk`, `mem_toAddSubgroup`, `coe_sSup_of_directedOn`, `instIsSemitopologicalRing`, `coe_center`, `mem_comap`, `centerToMulOpposite_symm_apply_coe`, `ValuationSubring.inv_mem_nonunits_iff`, `coe_equivMapOfInjective_apply`, `RingEquiv.ofLeftInverse'_apply`, `coe_eq_zero_iff`, `mem_map_equiv`, `ValuationSubring.mem_nonunits_iff_or`, `Subring.one_mem_toNonUnitalSubring`, `mem_prod`, `NonUnitalRingHom.coe_rangeRestrict`, `coe_centralizer`, `NonUnitalRingHom.rangeRestrict_surjective`, `mem_iInf`, `val_add`, `coe_set_mk`, `range_subtype`, `coe_map`, `ValuationSubring.mem_nonunits_iff`, `mem_toNonUnitalSubsemiring`, `mem_closure_iff`, `subset_closure`, `coe_comap`, `mem_mk'`, `add_mem`, `list_sum_mem`, `coe_iSup_of_directed`, `coe_inf`, `coe_toNonUnitalSubsemiring`, `mem_sInf`, `coe_toSubsemigroup`, `mem_closure`, `centralizer_eq_top_iff_subset`, `mem_nonUnitalSubalgebraOfNonUnitalSubring`, `multiset_sum_mem`, `coe_prod`, `sum_mem`, `centerToMulOpposite_apply_coe`, `NonUnitalSubalgebra.mem_toNonUnitalSubring`, `instIsMulCommutative_closure`, `closure_le_centralizer_centralizer`, `coe_copy`, `sub_mem`, `NonUnitalRingHom.mem_eqLocus`, `closure_le`
`mk'` 📖	CompOp	4 math math: `coe_mk'`, `mem_mk'`, `mk'_toAddSubgroup`, `mk'_toSubsemigroup`
`ofClass` 📖	CompOp	1 math math: `ofClass_carrier`
`toAddSubgroup` 📖	CompOp	9 math math: `toAddSubgroup_mono`, `toAddSubgroup_eq_top`, `toAddSubgroup_injective`, `coe_toAddSubgroup`, `mem_toAddSubgroup`, `sInf_toAddSubgroup`, `toAddSubgroup_strictMono`, `mk'_toAddSubgroup`, `toAddSubgroup_top`
`toNonUnitalCommRing` 📖	CompOp	—
`toNonUnitalRing` 📖	CompOp	6 math math: `instIsTopologicalRing`, `isMulCommutative_closure`, `RingEquiv.ofLeftInverse'_symm_apply`, `instIsSemitopologicalRing`, `RingEquiv.ofLeftInverse'_apply`, `instIsMulCommutative_closure`
`toNonUnitalSubsemiring` 📖	CompOp	11 math math: `toNonUnitalSubsemiring_eq_top`, `toNonUnitalSubsemiring_strictMono`, `centralizer_toNonUnitalSubsemiring`, `center_toNonUnitalSubsemiring`, `mem_carrier`, `toNonUnitalSubsemiring_top`, `mem_toNonUnitalSubsemiring`, `neg_mem'`, `coe_toNonUnitalSubsemiring`, `toNonUnitalSubsemiring_mono`, `toNonUnitalSubsemiring_injective`
`toSubsemigroup` 📖	CompOp	7 math math: `mem_toSubsemigroup`, `sInf_toSubsemigroup`, `toSubsemigroup_injective`, `toSubsemigroup_mono`, `coe_toSubsemigroup`, `toSubsemigroup_strictMono`, `mk'_toSubsemigroup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_mem` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`
`coe_copy` 📖	mathematical	`SetLike.coe` `NonUnitalSubring` `instSetLike`	`SetLike.coe` `NonUnitalSubring` `instSetLike` `copy`	—	—
`coe_eq_zero_iff` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `ZeroMemClass.zero` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`	—	`AddSubmonoidClass.toZeroMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`
`coe_mk'` 📖	mathematical	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Subsemigroup.instSetLike` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instSetLike`	`SetLike.coe` `NonUnitalSubring` `instSetLike` `mk'`	—	—
`coe_set_mk` 📖	mathematical	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	`SetLike.coe` `NonUnitalSubring` `instSetLike` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instSetLike`	—	—
`coe_toAddSubgroup` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instSetLike` `toAddSubgroup` `NonUnitalSubring` `instSetLike`	—	—
`coe_toNonUnitalSubsemiring` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instSetLike` `toNonUnitalSubsemiring` `NonUnitalSubring` `instSetLike`	—	—
`coe_toSubsemigroup` 📖	mathematical	—	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Subsemigroup.instSetLike` `toSubsemigroup` `NonUnitalSubring` `instSetLike`	—	—
`copy_eq` 📖	mathematical	`SetLike.coe` `NonUnitalSubring` `instSetLike`	`copy`	—	`SetLike.coe_injective`
`ext` 📖	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	—	—	`SetLike.ext`
`ext_iff` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	—	`ext`
`instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg` 📖	mathematical	—	`CanLift` `Set` `NonUnitalSubring` `SetLike.coe` `instSetLike` `Set.instMembership` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—
`instNonUnitalSubringClass` 📖	mathematical	—	`NonUnitalSubringClass` `NonUnitalSubring` `instSetLike`	—	`AddSubsemigroup.add_mem'` `AddSubmonoid.zero_mem'` `NonUnitalSubsemiring.mul_mem'` `neg_mem'`
`mem_carrier` 📖	mathematical	—	`NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `toNonUnitalSubsemiring` `NonUnitalSubring` `instSetLike`	—	—
`mem_mk` 📖	mathematical	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instSetLike`	—	—
`mem_mk'` 📖	mathematical	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Subsemigroup.instSetLike` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `mk'` `Set` `Set.instMembership`	—	—
`mem_toAddSubgroup` 📖	mathematical	—	`AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `toAddSubgroup` `NonUnitalSubring` `instSetLike`	—	—
`mem_toNonUnitalSubsemiring` 📖	mathematical	—	`NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `NonUnitalSubsemiring.instSetLike` `toNonUnitalSubsemiring` `NonUnitalSubring` `instSetLike`	—	—
`mem_toSubsemigroup` 📖	mathematical	—	`Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `SetLike.instMembership` `Subsemigroup.instSetLike` `toSubsemigroup` `NonUnitalSubring` `instSetLike`	—	—
`mk'_toAddSubgroup` 📖	mathematical	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Subsemigroup.instSetLike` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instSetLike`	`toAddSubgroup` `mk'`	—	`SetLike.coe_injective`
`mk'_toSubsemigroup` 📖	mathematical	`SetLike.coe` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Subsemigroup.instSetLike` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `AddSubgroup.instSetLike`	`toSubsemigroup` `mk'`	—	`SetLike.coe_injective`
`mk_le_mk` 📖	mathematical	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	`NonUnitalSubring` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubsemiring.instPartialOrder`	—	—
`mul_mem` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`MulMemClass.mul_mem` `NonUnitalSubsemiringClass.mulMemClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`
`neg_mem` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	`NegMemClass.neg_mem` `NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClass`
`neg_mem'` 📖	mathematical	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `toNonUnitalSubsemiring`	`Set` `Set.instMembership` `AddSubsemigroup.carrier` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddSubmonoid.toAddSubsemigroup` `NonUnitalSubsemiring.toAddSubmonoid` `toNonUnitalSubsemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`ofClass_carrier` 📖	mathematical	—	`SetLike.coe` `NonUnitalSubring` `instSetLike` `ofClass`	—	—
`sub_mem` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`sub_mem` `NonUnitalSubringClass.addSubgroupClass` `instNonUnitalSubringClass`
`toAddSubgroup_injective` 📖	mathematical	—	`NonUnitalSubring` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `toAddSubgroup`	—	`ext` `SetLike.ext_iff`
`toAddSubgroup_mono` 📖	mathematical	—	`Monotone` `NonUnitalSubring` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `PartialOrder.toPreorder` `instPartialOrder` `AddSubgroup.instPartialOrder` `toAddSubgroup`	—	`StrictMono.monotone` `toAddSubgroup_strictMono`
`toAddSubgroup_strictMono` 📖	mathematical	—	`StrictMono` `NonUnitalSubring` `AddSubgroup` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `PartialOrder.toPreorder` `instPartialOrder` `AddSubgroup.instPartialOrder` `toAddSubgroup`	—	—
`toNonUnitalSubsemiring_injective` 📖	mathematical	—	`NonUnitalSubring` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalSubsemiring`	—	`ext` `SetLike.ext_iff`
`toNonUnitalSubsemiring_mono` 📖	mathematical	—	`Monotone` `NonUnitalSubring` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `PartialOrder.toPreorder` `instPartialOrder` `NonUnitalSubsemiring.instPartialOrder` `toNonUnitalSubsemiring`	—	`StrictMono.monotone` `toNonUnitalSubsemiring_strictMono`
`toNonUnitalSubsemiring_strictMono` 📖	mathematical	—	`StrictMono` `NonUnitalSubring` `NonUnitalSubsemiring` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `PartialOrder.toPreorder` `instPartialOrder` `NonUnitalSubsemiring.instPartialOrder` `toNonUnitalSubsemiring`	—	—
`toSubsemigroup_injective` 📖	mathematical	—	`NonUnitalSubring` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toSubsemigroup`	—	`ext` `SetLike.ext_iff`
`toSubsemigroup_mono` 📖	mathematical	—	`Monotone` `NonUnitalSubring` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Subsemigroup.instPartialOrder` `toSubsemigroup`	—	`StrictMono.monotone` `toSubsemigroup_strictMono`
`toSubsemigroup_strictMono` 📖	mathematical	—	`StrictMono` `NonUnitalSubring` `Subsemigroup` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `PartialOrder.toPreorder` `instPartialOrder` `Subsemigroup.instPartialOrder` `toSubsemigroup`	—	—
`val_add` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubringClass.toNonUnitalNonAssocRing` `instNonUnitalSubringClass`	—	`instNonUnitalSubringClass`
`val_mul` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalSubringClass.toNonUnitalNonAssocRing` `instNonUnitalSubringClass`	—	`instNonUnitalSubringClass`
`val_neg` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `NegMemClass.neg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClass`	—	`NonUnitalSubringClass.toNegMemClass` `instNonUnitalSubringClass`
`val_zero` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `ZeroMemClass.zero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `AddSubmonoidClass.toZeroMemClass` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`	—	`AddSubmonoidClass.toZeroMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`
`zero_mem` 📖	mathematical	—	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `NonUnitalSubringClass.toNonUnitalSubsemiringClass` `instNonUnitalSubringClass`
`zsmul_mem` 📖	mathematical	`NonUnitalSubring` `SetLike.instMembership` `instSetLike`	`NonUnitalSubring` `SetLike.instMembership` `instSetLike` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`zsmul_mem` `NonUnitalSubringClass.addSubgroupClass` `instNonUnitalSubringClass`

NonUnitalSubringClass

Definitions

Name	Category	Theorems
`subtype` 📖	CompOp	6 math math: `coe_subtype`, `NonUnitalSubalgebra.toSubring_subtype`, `NonUnitalStarSubalgebra.toSubring_subtype`, `NonUnitalSubring.range_subtype`, `subtype_apply`, `subtype_injective`
`toNonUnitalCommRing` 📖	CompOp	—
`toNonUnitalNonAssocCommRing` 📖	CompOp	—
`toNonUnitalNonAssocRing` 📖	CompOp	13 math math: `coe_subtype`, `NonUnitalSubring.topEquiv_symm_apply_coe`, `NonUnitalSubring.topEquiv_apply`, `NonUnitalSubring.val_mul`, `NonUnitalSubalgebra.toSubring_subtype`, `NonUnitalSubring.coe_equivMapOfInjective_apply`, `NonUnitalRingHom.coe_rangeRestrict`, `NonUnitalStarSubalgebra.toSubring_subtype`, `NonUnitalRingHom.rangeRestrict_surjective`, `NonUnitalSubring.val_add`, `NonUnitalSubring.range_subtype`, `subtype_apply`, `subtype_injective`
`toNonUnitalRing` 📖	CompOp	4 math math: `NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe`, `NonUnitalSubring.unitization_apply`, `NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe`, `NonUnitalSubring.unitization_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addSubgroupClass` 📖	mathematical	—	`AddSubgroupClass` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `NonUnitalNonAssocRing.toAddCommGroup`	—	`NonUnitalSubsemiringClass.toAddSubmonoidClass` `toNonUnitalSubsemiringClass` `toNegMemClass`
`coe_subtype` 📖	mathematical	—	`DFunLike.coe` `NonUnitalRingHom` `SetLike.instMembership` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `NonUnitalRingHom.instFunLike` `subtype`	—	—
`subtype_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalRingHom` `SetLike.instMembership` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `NonUnitalRingHom.instFunLike` `subtype`	—	—
`subtype_injective` 📖	mathematical	—	`SetLike.instMembership` `DFunLike.coe` `NonUnitalRingHom` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `toNonUnitalNonAssocRing` `NonUnitalRingHom.instFunLike` `subtype`	—	`Subtype.coe_injective`
`toNegMemClass` 📖	mathematical	—	`NegMemClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NonUnitalNonAssocRing.toAddCommGroup`	—	—
`toNonUnitalSubsemiringClass` 📖	mathematical	—	`NonUnitalSubsemiringClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	—

(root)

Definitions

Name	Category	Theorems
`NonUnitalSubring` 📖	CompData	159 math math: `NonUnitalSubring.instIsTopologicalRing`, `NonUnitalSubring.mem_closure_of_mem`, `NonUnitalSubring.coe_top`, `NonUnitalSubring.toNonUnitalSubsemiring_eq_top`, `NonUnitalSubring.toAddSubgroup_mono`, `ValuationSubring.image_maximalIdeal`, `NonUnitalSubring.coe_sInf`, `NonUnitalRingHom.mem_range`, `NonUnitalSubring.map_inf`, `NonUnitalSubring.toNonUnitalSubsemiring_strictMono`, `NonUnitalSubring.mem_centralizer_iff`, `NonUnitalSubring.prod_top`, `NonUnitalSubring.ext_iff`, `NonUnitalSubring.eq_top_iff'`, `ValuationSubring.nonunits_subset`, `NonUnitalSubring.closure_preimage_le`, `NonUnitalSubalgebra.coe_toNonUnitalSubring`, `NonUnitalSubring.topologicalClosure_minimal`, `NonUnitalSubring.map_iSup`, `NonUnitalSubring.centerCongr_apply_coe`, `NonUnitalSubring.mem_sSup_of_directedOn`, `NonUnitalSubring.closure_empty`, `NonUnitalStarSubalgebra.coe_toNonUnitalSubring`, `NonUnitalSubring.comap_top`, `NonUnitalSubring.zero_mem`, `NonUnitalSubring.mem_top`, `NonUnitalSubring.mem_inf`, `NonUnitalSubring.mem_center_iff`, `NonUnitalSubring.topEquiv_symm_apply_coe`, `NonUnitalRingHom.eqLocus_same`, `NonUnitalRingHom.eqOn_set_closure`, `NonUnitalSubring.isMulCommutative_closure`, `ValuationSubring.nonunits_injective`, `NonUnitalSubring.closure_univ`, `NonUnitalSubring.neg_mem`, `NonUnitalSubring.coe_mk'`, `NonUnitalSubring.center_eq_top`, `Ideal.image_subset_nonunits_valuationSubring`, `NonUnitalSubring.mem_iSup_of_directed`, `NonUnitalSubring.isClosed_topologicalClosure`, `NonUnitalRingHom.mem_range_self`, `NonUnitalSubring.topEquiv_apply`, `NonUnitalStarSubalgebra.mem_toNonUnitalSubring`, `NonUnitalSubring.ofClass_carrier`, `NonUnitalSubring.val_mul`, `NonUnitalSubring.centralizer_le`, `NonUnitalSubring.map_sup`, `NonUnitalSubring.closure_eq`, `NonUnitalSubring.closure_sUnion`, `NonUnitalSubring.toAddSubgroup_eq_top`, `NonUnitalSubring.coe_iInf`, `NonUnitalSubring.closure_mono`, `NonUnitalSubalgebra.toNonUnitalSubring_injective`, `NonUnitalSubring.topologicalClosure_mono`, `NonUnitalSubring.mem_toSubsemigroup`, `NonUnitalSubring.zsmul_mem`, `NonUnitalSubring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg`, `NonUnitalSubring.val_zero`, `NonUnitalSubring.centerCongr_symm_apply_coe`, `NonUnitalRingHom.range_eq_top`, `NonUnitalSubring.toAddSubgroup_injective`, `ValuationSubring.nonunits_le_nonunits`, `NonUnitalSubring.sInf_toSubsemigroup`, `NonUnitalSubring.instNonUnitalSubringClass`, `NonUnitalSubring.coe_toAddSubgroup`, `NonUnitalSubring.map_le_iff_le_comap`, `NonUnitalSubring.toSubsemigroup_injective`, `NonUnitalSubring.top_prod`, `NonUnitalSubring.prod_mono_left`, `NonUnitalSubring.val_neg`, `NonUnitalSubring.mk_le_mk`, `NonUnitalSubring.mem_bot`, `NonUnitalSubring.mem_carrier`, `NonUnitalSubring.coe_bot`, `NonUnitalSubring.mem_map`, `NonUnitalRingHom.coe_range`, `NonUnitalSubring.map_bot`, `NonUnitalSubring.top_prod_top`, `NonUnitalSubring.prod_mono`, `NonUnitalSubring.mul_mem`, `NonUnitalSubring.toNonUnitalSubsemiring_top`, `ValuationSubring.coe_mem_nonunits_iff`, `ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal`, `RingEquiv.ofLeftInverse'_symm_apply`, `NonUnitalSubring.mem_mk`, `NonUnitalSubring.closure_union`, `NonUnitalSubring.mem_toAddSubgroup`, `NonUnitalSubring.coe_sSup_of_directedOn`, `NonUnitalSubring.instIsSemitopologicalRing`, `NonUnitalSubring.coe_center`, `NonUnitalSubring.mem_comap`, `NonUnitalSubring.centerToMulOpposite_symm_apply_coe`, `NonUnitalRingHom.range_eq_top_of_surjective`, `ValuationSubring.inv_mem_nonunits_iff`, `NonUnitalSubring.coe_equivMapOfInjective_apply`, `RingEquiv.ofLeftInverse'_apply`, `NonUnitalSubring.coe_eq_zero_iff`, `NonUnitalSubring.closure_iUnion`, `NonUnitalSubring.mem_map_equiv`, `NonUnitalSubring.toSubsemigroup_mono`, `ValuationSubring.mem_nonunits_iff_or`, `Subring.one_mem_toNonUnitalSubring`, `NonUnitalSubring.mem_prod`, `NonUnitalRingHom.coe_rangeRestrict`, `NonUnitalSubring.coe_centralizer`, `NonUnitalAlgebra.to_subring_eq_top`, `NonUnitalRingHom.rangeRestrict_surjective`, `NonUnitalAlgebra.toNonUnitalSubring_eq_top`, `NonUnitalSubring.mem_iInf`, `NonUnitalSubring.val_add`, `NonUnitalSubring.coe_set_mk`, `ValuationSubring.nonunits_le`, `NonUnitalSubring.comap_iInf`, `NonUnitalSubring.range_subtype`, `NonUnitalSubring.sInf_toAddSubgroup`, `NonUnitalSubring.coe_map`, `ValuationSubring.mem_nonunits_iff`, `NonUnitalSubring.mem_toNonUnitalSubsemiring`, `NonUnitalSubring.comap_inf`, `NonUnitalSubring.mem_closure_iff`, `NonUnitalSubring.toAddSubgroup_strictMono`, `NonUnitalSubring.subset_closure`, `NonUnitalSubring.coe_comap`, `NonUnitalSubring.mem_mk'`, `NonUnitalSubring.gc_map_comap`, `NonUnitalSubring.add_mem`, `NonUnitalSubring.list_sum_mem`, `NonUnitalSubring.coe_iSup_of_directed`, `NonUnitalSubring.coe_inf`, `NonUnitalSubring.coe_toNonUnitalSubsemiring`, `NonUnitalSubring.mem_sInf`, `NonUnitalSubring.center_le_centralizer`, `NonUnitalAlgebra.top_toSubring`, `NonUnitalRingHom.range_eq_map`, `NonUnitalSubring.coe_toSubsemigroup`, `NonUnitalSubring.mem_closure`, `NonUnitalSubring.centralizer_eq_top_iff_subset`, `mem_nonUnitalSubalgebraOfNonUnitalSubring`, `NonUnitalSubring.prod_mono_right`, `NonUnitalAlgebra.toNonUnitalSubring_top`, `NonUnitalSubring.multiset_sum_mem`, `NonUnitalSubring.coe_prod`, `NonUnitalSubring.sum_mem`, `NonUnitalSubring.centerToMulOpposite_apply_coe`, `NonUnitalSubalgebra.mem_toNonUnitalSubring`, `NonUnitalSubring.toSubsemigroup_strictMono`, `NonUnitalSubring.instIsMulCommutative_closure`, `NonUnitalRingHom.closure_preimage_le`, `NonUnitalSubring.toAddSubgroup_top`, `NonUnitalSubring.closure_le_centralizer_centralizer`, `NonUnitalStarSubalgebra.toNonUnitalSubring_injective`, `NonUnitalSubring.coe_copy`, `NonUnitalSubring.toNonUnitalSubsemiring_mono`, `NonUnitalSubring.toNonUnitalSubsemiring_injective`, `NonUnitalSubring.sub_mem`, `NonUnitalSubring.map_iInf`, `NonUnitalRingHom.mem_eqLocus`, `NonUnitalSubring.le_topologicalClosure`, `NonUnitalSubring.closure_le`
`NonUnitalSubringClass` 📖	CompData	6 math math: `SubringClass.nonUnitalSubringClass`, `NonUnitalStarSubalgebra.instNonUnitalSubringClass`, `instNonUnitalSubringClassTwoSidedIdeal`, `NonUnitalSubring.instNonUnitalSubringClass`, `instNonUnitalSubringClassIdeal`, `NonUnitalSubalgebra.instNonUnitalSubringClass`

---

← Back to Index