Defs

📁 Source: Mathlib/Algebra/Ring/Subsemiring/Defs.lean

Statistics

Metric	Count
Definitions AddSubmonoidWithOneClass, toAddMonoidWithOne, toSubsemiring, domRestrict, eqLocusS, copy, instMin, instPartialOrder, instSetLike, instTop, mk', ofClass, subtype, toAddSubmonoid, toCommSemiring, toNonAssocSemiring, toNonUnitalSubsemiring, toSemiring, toSubmonoid, SubsemiringClass, subtype, toCommSemiring, toNonAssocSemiring, toSemiring	24
Theorems toAddSubmonoidClass, toOneMemClass, toSubsemiring_toNonUnitalSubsemiring, eqLocusS_same, mem_eqLocusS, restrict_apply, add_mem, add_mem', coe_add, coe_carrier_toSubmonoid, coe_copy, coe_inf, coe_mk', coe_mul, coe_ofClass, coe_one, coe_pow, coe_set_mk, coe_subtype, coe_toAddSubmonoid, coe_toNonUnitalSubsemiring, coe_toSubmonoid, coe_top, coe_zero, copy_eq, copy_toSubmonoid, ext, ext_iff, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul, instSubsemiringClass, mem_carrier, mem_inf, mem_mk, mem_mk', mem_toAddSubmonoid, mem_toNonUnitalSubsemiring, mem_toSubmonoid, mem_top, mk'_toAddSubmonoid, mk'_toSubmonoid, mul_mem, noZeroDivisors, nontrivial, nsmul_mem, one_mem, one_mem_toNonUnitalSubsemiring, pow_mem, subtype_apply, subtype_injective, toAddSubmonoid_injective, toNonUnitalSubsemiring_inj, toNonUnitalSubsemiring_injective, toNonUnitalSubsemiring_toSubsemiring, toSubmonoid_injective, zero_mem, zero_mem', addSubmonoidWithOneClass, coe_subtype, noZeroDivisors, nonUnitalSubsemiringClass, nontrivial, subtype_apply, subtype_injective, toAddSubmonoidClass, toSubmonoidClass, natCast_mem, ofNat_mem	67
Total	91

AddSubmonoidWithOneClass

Definitions

Name	Category	Theorems
toAddMonoidWithOne 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddSubmonoidClass 📖	mathematical	—	AddSubmonoidClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid	—	—
toOneMemClass 📖	mathematical	—	OneMemClass AddMonoidWithOne.toOne	—	—

NonUnitalSubsemiring

Definitions

Name	Category	Theorems
toSubsemiring 📖	CompOp	2 math math: Subsemiring.toNonUnitalSubsemiring_toSubsemiring, toSubsemiring_toNonUnitalSubsemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toSubsemiring_toNonUnitalSubsemiring 📖	mathematical	NonUnitalSubsemiring NonAssocSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	Subsemiring.toNonUnitalSubsemiring toSubsemiring	—	—

RingHom

Definitions

Name	Category	Theorems
domRestrict 📖	CompOp	1 math math: restrict_apply
eqLocusS 📖	CompOp	2 math math: mem_eqLocusS, eqLocusS_same

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eqLocusS_same 📖	mathematical	—	eqLocusS Top.top Subsemiring Subsemiring.instTop	—	SetLike.ext
mem_eqLocusS 📖	mathematical	—	Subsemiring SetLike.instMembership Subsemiring.instSetLike eqLocusS DFunLike.coe RingHom instFunLike	—	—
restrict_apply 📖	mathematical	—	DFunLike.coe RingHom SetLike.instMembership SubsemiringClass.toNonAssocSemiring instFunLike domRestrict	—	—

Subsemiring

Definitions

Name	Category	Theorems
copy 📖	CompOp	3 math math: copy_eq, coe_copy, copy_toSubmonoid
instMin 📖	CompOp	8 math math: mem_inf, map_comap_eq, map_inf, op_inf, comap_inf, coe_inf, unop_inf, Algebra.inf_toSubsemiring
instPartialOrder 📖	CompOp	43 math math: closure_le, centralizer_le, closure_mono, RingPreordering.toSubsemiring_strictMono, gc_map_comap, RingPreordering.toSubsemiring_lt_toSubsemiring, op_le_op_iff, homogeneousCore_mono, le_op_iff, Subring.toSubsemiring_mono, Subring.toSubsemiring_lt_toSubsemiring, unop_le_unop_iff, StarSubsemiring.toSubsemiring_le_iff, prod_mono_right, opEquiv_apply, RingPreordering.toSubsemiring_mono, Subring.toSubsemiring_le_toSubsemiring, toSubmonoid_mono, closure_le_centralizer_centralizer, op_le_iff, RingPreordering.toSubsemiring_le_toSubsemiring, pointwise_smul_subset_iff, toSubmonoid_strictMono, opEquiv_symm_apply, Subring.toSubsemiring_strictMono, RingHom.sclosure_preimage_le, StarSubalgebra.rangeS_le, pointwise_smul_le_pointwise_smul_iff, toSubsemiring_homogeneousCore_le, instCovariantClassHSMulLe, Subring.mk_le_mk, toAddSubmonoid_mono, prod_mono_left, subset_pointwise_smul_iff, le_topologicalClosure, map_le_iff_le_comap, toAddSubmonoid_strictMono, pointwise_smul_le_pointwise_smul_iff₀, le_centralizer_centralizer, pointwise_smul_le_iff₀, Subalgebra.rangeS_le, le_pointwise_smul_iff₀, center_le_centralizer
instSetLike 📖	CompOp	197 math math: RingCone.coe_set_mk, mem_sumSq, mem_toNonUnitalSubsemiring, mem_sSup_of_directedOn, mem_top, coe_subtype, Polynomial.mem_lifts_iff_mem_alg, closure_le, eq_top_iff', isClosed_topologicalClosure, RingPreordering.mem_mk, coe_pow, mem_carrier, mem_iInf, Polynomial.monomial_mem_lifts, CentroidHom.star_centerToCentroidCenter, mem_closure, Polynomial.X_mem_lifts, toIsOrderedRing, mem_smul_pointwise_iff_exists, StarSubsemiring.mem_toSubsemiring, smul_mem_pointwise_smul_iff, Subring.coe_toSubsemiring, mem_bot, nontrivial, Submonoid.subsemiringClosure_coe, RingHom.rangeSRestrict_surjective, centerCongr_symm_apply_coe, IsScalarTower.subsemiring, mem_subalgebraOfSubsemiring, Polynomial.Splits.mem_lift_of_roots_mem_range, coe_prod, RingEquiv.ofLeftInverseS_symm_apply, addEquivOp_apply_coe, isScalarTower, Subring.mopRingEquivOp_apply_coe, RingCon.comapQuotientEquivRangeS_symm_mk, RingHom.coe_rangeSRestrict, mem_iSup_of_directed, smul_def, coe_iSup_of_directed, coe_equivMapOfInjective_apply, Subalgebra.mopAlgEquivOp_symm_apply, coe_sInf, toIsStrictOrderedRing, coe_add, coe_one, isArtinianRing_rangeS, Subring.mem_toSubsemiring, Polynomial.C_mem_lifts, mem_inf, RingCone.mem_mk, mem_mk', coe_toSubmonoid, subset_closure, centerCongr_apply_coe, one_mem, StarSubsemiring.coe_toSubsemiring, closure_le_centralizer_centralizer, Polynomial.mem_lifts, noZeroDivisors, Subalgebra.linearEquivOp_apply_coe, mem_map_equiv, Polynomial.lifts_iff_ringHom_rangeS, Subring.topEquiv_apply, RingEquiv.subsemiringMap_apply_coe, mem_op, Subring.coe_set_mk, HomogeneousSubsemiring.mem_iff, Subring.mopRingEquivOp_symm_apply, centerToMulOpposite_symm_apply_coe, IsHomogeneous.subsemiringClosure, addEquivOp_symm_apply_coe, coe_carrier_toSubmonoid, Polynomial.C'_mem_lifts, smul_mem_pointwise_smul_iff₀, mem_centralizer_iff, centerToMulOpposite_apply_coe, isHomogeneous_iff_subset_iInter, RingPreordering.coe_toSubsemiring, RingEquiv.subsemiringMap_symm_apply_coe, RingCon.comapQuotientEquivRangeS_mk, Subring.topEquiv_symm_apply_coe, ext_iff, center.smulCommClass_right, RingCon.coe_quotientKerEquivRangeS_mk, rangeS_subtype, comap_toSubmonoid, coe_sumSq, mem_inv_pointwise_smul_iff₀, RingHom.mem_rangeS, Subalgebra.mem_mk, closure_eq, mem_comap, StarSubsemiring.coe_mk, inclusion_injective, Subalgebra.coe_toSubsemiring, CharP.subsemiring, mopRingEquivOp_apply_coe, IsLocalization.scaleRoots_commonDenom_mem_lifts, zero_mem, instSMulCommClassSubtypeMemCenter_1, coe_inf, instSubsemiringClass, coe_toNonUnitalSubsemiring, isHomogeneous_iff_forall_subset, coe_top, Subalgebra.coe_valA, RingHom.mem_rangeS_self, smulCommClass_left, Subalgebra.algEquivOpMop_apply, Polynomial.lifts_iff_coeff_lifts, mem_toSubmonoid, coe_centralizer, coe_pointwise_smul, Subring.ringEquivOpMop_symm_apply_coe, Subalgebra.mem_toSubsemiring, mem_closure_iff_exists_list, mem_toAddSubmonoid, map_toSubmonoid, isNoetherianRing_rangeS, RingPreordering.mem_toSubsemiring, topologicalSemiring, Algebra.algebraMap_ofSubsemiring, ringEquivOpMop_symm_apply_coe, instSMulCommClassSubtypeMemCenter, Polynomial.X_pow_mem_lifts, coe_closure_eq, topologicalClosure_coe, mem_pointwise_smul_iff_inv_smul_mem, mem_map, NonUnitalNonAssocSemiring.mem_center_iff, HomogeneousSubsemiring.is_homogeneous', coe_ofClass, coe_sSup_of_directedOn, coe_matrix, Polynomial.lifts_iff_liftsRing, mem_mk, topEquiv_symm_apply_coe, coe_op, coe_zero, coe_set_mk, centralizer_eq_top_iff_subset, CentroidHom.centerToCentroidCenter_apply, coe_mk', Subalgebra.linearEquivOp_symm_apply_coe, Subring.mem_mk, ringEquivOpMop_apply, subtype_apply, RingEquiv.ofLeftInverseS_apply, Submonoid.subsemiringClosure_mem, continuousSMul, subtype_injective, coe_toAddSubmonoid, Polynomial.lifts_iff_set_range, Subalgebra.mem_perfectClosure_iff, smulCommClass_right, le_centralizer_centralizer, mopRingEquivOp_symm_apply, coe_iInf, coe_center, Algebra.IsInvariant.charpoly_mem_lifts, topEquiv_apply, coe_map, Module.End.mem_subsemiringCenter_iff, mem_closure_of_mem, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul, RingHom.mem_eqLocusS, coe_mul, mem_center_iff, Subalgebra.mopAlgEquivOp_apply_coe, Subalgebra.coe_mk, faithfulSMul, RingHom.eqOn_sclosure, Subalgebra.algEquivOpMop_symm_apply_coe, Subring.ringEquivOpMop_apply, mem_pointwise_smul_iff_inv_smul_mem₀, mem_prod, mem_nonneg, mem_unop, IsHomogeneous.subsemiringClosure_of_isHomogeneousElem, Polynomial.mem_lift_of_splits_of_roots_mem_range, integralClosure.mem_lifts_of_monic_of_dvd_map, Polynomial.lifts_iff_coeffs_subset_range, mem_closure_iff, Polynomial.mem_map_rangeS, Subalgebra.coe_valA', mem_inv_pointwise_smul_iff, coe_nonneg, RingHom.coe_rangeS, coe_unop, mem_sInf, coe_comap, RingHom.ker_rangeSRestrict, coe_bot, RingPreordering.coe_set_mk, center.smulCommClass_left
instTop 📖	CompOp	33 math math: Subring.range_snd, mem_top, eq_top_iff', RingHom.rangeS_eq_top, op_eq_top, Algebra.toSubsemiring_eq_top, center_eq_top, RingHom.rangeS_toSubmonoid, prod_top, unop_eq_top, Subring.toSubsemiring_top, Subring.topEquiv_apply, top_prod_top, comap_top, Subring.topEquiv_symm_apply_coe, RingHom.rangeS_eq_map, range_fst, RingHom.rangeS_top_iff_surjective, Algebra.top_toSubsemiring, RingHom.rangeS_top_of_surjective, coe_top, unop_top, range_snd, closure_univ, topEquiv_symm_apply_coe, centralizer_eq_top_iff_subset, RingCon.rangeS_mk', Subring.range_fst, top_prod, op_top, topEquiv_apply, Subring.toSubsemiring_eq_top, RingHom.eqLocusS_same
mk' 📖	CompOp	4 math math: mem_mk', mk'_toAddSubmonoid, coe_mk', mk'_toSubmonoid
ofClass 📖	CompOp	2 math math: RingHom.surjective_codRestrict, coe_ofClass
subtype 📖	CompOp	8 math math: coe_subtype, rangeS_subtype, Subalgebra.coe_valA, Algebra.algebraMap_ofSubsemiring, subtype_apply, subtype_injective, Subalgebra.toSubsemiring_subtype, Subalgebra.coe_valA'
toAddSubmonoid 📖	CompOp	15 math math: Submonoid.subsemiringClosure_toAddSubmonoid, pointwise_smul_toAddSubmonoid, Subring.coe_matrix, sInf_toAddSubmonoid, mk'_toAddSubmonoid, Subalgebra.coe_matrix, AlgEquiv.subalgebraMap_apply_coe, mem_toAddSubmonoid, toAddSubmonoid_mono, coe_matrix, toAddSubmonoid_injective, nonneg_toAddSubmonoid, toAddSubmonoid_strictMono, coe_toAddSubmonoid, AlgEquiv.subalgebraMap_symm_apply_coe
toCommSemiring 📖	CompOp	1 math math: Algebra.algebraMap_ofSubsemiring
toNonAssocSemiring 📖	CompOp	41 math math: coe_subtype, CentroidHom.star_centerToCentroidCenter, RingHom.rangeSRestrict_surjective, centerCongr_symm_apply_coe, RingEquiv.ofLeftInverseS_symm_apply, addEquivOp_apply_coe, RingCon.comapQuotientEquivRangeS_symm_mk, RingHom.coe_rangeSRestrict, coe_equivMapOfInjective_apply, Subalgebra.mopAlgEquivOp_symm_apply, coe_add, centerCongr_apply_coe, noZeroDivisors, RingEquiv.subsemiringMap_apply_coe, Subring.mopRingEquivOp_symm_apply, centerToMulOpposite_symm_apply_coe, addEquivOp_symm_apply_coe, centerToMulOpposite_apply_coe, RingEquiv.subsemiringMap_symm_apply_coe, RingCon.comapQuotientEquivRangeS_mk, RingCon.coe_quotientKerEquivRangeS_mk, rangeS_subtype, inclusion_injective, CharP.subsemiring, mopRingEquivOp_apply_coe, Subalgebra.coe_valA, Subalgebra.algEquivOpMop_apply, topologicalSemiring, ringEquivOpMop_symm_apply_coe, topEquiv_symm_apply_coe, CentroidHom.centerToCentroidCenter_apply, ringEquivOpMop_apply, subtype_apply, RingEquiv.ofLeftInverseS_apply, subtype_injective, mopRingEquivOp_symm_apply, topEquiv_apply, coe_mul, Subring.ringEquivOpMop_apply, Subalgebra.coe_valA', RingHom.ker_rangeSRestrict
toNonUnitalSubsemiring 📖	CompOp	9 math math: mem_toNonUnitalSubsemiring, sumSq_toNonUnitalSubsemiring, toNonUnitalSubsemiring_toSubsemiring, coe_toNonUnitalSubsemiring, toNonUnitalSubsemiring_injective, one_mem_toNonUnitalSubsemiring, toNonUnitalSubsemiring_inj, NonUnitalSubsemiring.toSubsemiring_toNonUnitalSubsemiring, Submonoid.subsemiringClosure_toNonUnitalSubsemiring
toSemiring 📖	CompOp	6 math math: toIsOrderedRing, toIsStrictOrderedRing, isArtinianRing_rangeS, Subalgebra.coe_valA, isNoetherianRing_rangeS, RingHom.ker_rangeSRestrict
toSubmonoid 📖	CompOp	57 math math: RingPreordering.ext_iff, mem_carrier, Subalgebra.coe_toAddSubmonoid, Subring.addEquivOp_apply_coe, IntermediateField.mem_carrier, StarSubalgebra.toNonUnitalStarSubalgebra_toStarSubalgebra, addEquivOp_apply_coe, Subring.toSubmonoid_mono, RingHom.rangeS_toSubmonoid, Subring.mopRingEquivOp_apply_coe, Subring.mk'_toSubmonoid, coe_toSubmonoid, VonNeumannAlgebra.centralizer_centralizer', toSubmonoid_mono, StarSubsemiring.mem_carrier, Subalgebra.linearEquivOp_apply_coe, Subalgebra.mem_carrier, ValuationSubring.mem_carrier, addEquivOp_symm_apply_coe, coe_carrier_toSubmonoid, center_toSubmonoid, Subalgebra.algebraMap_mem', toSubmonoid_strictMono, comap_toSubmonoid, RingPreordering.neg_one_notMem', Subfield.coe_inf, mopRingEquivOp_apply_coe, StarSubalgebra.mem_carrier, centralizer_toSubmonoid, mem_toSubmonoid, ValuationSubring.mem_or_inv_mem', Subring.mem_carrier, Subring.toSubmonoid_strictMono, Subring.ringEquivOpMop_symm_apply_coe, map_toSubmonoid, Subring.coe_toSubmonoid, ringEquivOpMop_symm_apply_coe, RingPreordering.mem_of_isSquare', Subfield.mem_toSubmonoid, op_toSubmonoid, zero_mem', Subalgebra.linearEquivOp_symm_apply_coe, Subring.sInf_toSubmonoid, copy_toSubmonoid, sInf_toSubmonoid, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, Subring.mem_toSubmonoid, toSubmonoid_injective, mk'_toSubmonoid, Subalgebra.mopAlgEquivOp_apply_coe, Subalgebra.algEquivOpMop_symm_apply_coe, unop_toSubmonoid, Subfield.mem_carrier, Subfield.coe_toSubmonoid, Subring.addEquivOp_symm_apply_coe, Subring.toSubmonoid_injective, Subring.centralizer_toSubmonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem 📖	mathematical	Subsemiring SetLike.instMembership instSetLike	Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass instSubsemiringClass
add_mem' 📖	mathematical	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.toSubsemigroup toSubmonoid	AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
coe_add 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring toNonAssocSemiring	—	—
coe_carrier_toSubmonoid 📖	mathematical	—	Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.toSubsemigroup toSubmonoid SetLike.coe Subsemiring instSetLike	—	—
coe_copy 📖	mathematical	SetLike.coe Subsemiring instSetLike	copy	—	—
coe_inf 📖	mathematical	—	SetLike.coe Subsemiring instSetLike instMin Set Set.instInter	—	—
coe_mk' 📖	mathematical	SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike AddSubmonoid AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoid.instSetLike	Subsemiring instSetLike mk'	—	—
coe_mul 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring toNonAssocSemiring	—	—
coe_ofClass 📖	mathematical	—	SetLike.coe Subsemiring instSetLike ofClass	—	—
coe_one 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike OneMemClass.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass instSubsemiringClass	—	AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass instSubsemiringClass
coe_pow 📖	mathematical	—	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike SubmonoidClass.nPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SubsemiringClass.toSubmonoidClass instSubsemiringClass Monoid.toNatPow	—	SubsemiringClass.toSubmonoidClass instSubsemiringClass
coe_set_mk 📖	mathematical	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.toSubsemigroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddZero.toZero	SetLike.coe Subsemiring instSetLike Submonoid Submonoid.instSetLike	—	—
coe_subtype 📖	mathematical	—	DFunLike.coe RingHom Subsemiring SetLike.instMembership instSetLike toNonAssocSemiring RingHom.instFunLike subtype	—	—
coe_toAddSubmonoid 📖	mathematical	—	SetLike.coe AddSubmonoid AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoid.instSetLike toAddSubmonoid Subsemiring instSetLike	—	—
coe_toNonUnitalSubsemiring 📖	mathematical	—	SetLike.coe NonUnitalSubsemiring NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalSubsemiring.instSetLike toNonUnitalSubsemiring Subsemiring instSetLike	—	—
coe_toSubmonoid 📖	mathematical	—	SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike toSubmonoid Subsemiring instSetLike	—	—
coe_top 📖	mathematical	—	SetLike.coe Subsemiring instSetLike Top.top instTop Set.univ	—	—
coe_zero 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SubsemiringClass.toAddSubmonoidClass instSubsemiringClass	—	AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass instSubsemiringClass
copy_eq 📖	mathematical	SetLike.coe Subsemiring instSetLike	copy	—	SetLike.coe_injective
copy_toSubmonoid 📖	mathematical	SetLike.coe Subsemiring instSetLike	toSubmonoid copy MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MulOne.toMul MulOneClass.toMulOne	—	—
ext 📖	—	Subsemiring SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike	—	ext
instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul 📖	mathematical	—	CanLift Set Subsemiring SetLike.coe instSetLike Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
instSubsemiringClass 📖	mathematical	—	SubsemiringClass Subsemiring instSetLike	—	Subsemigroup.mul_mem' Submonoid.one_mem' AddSubsemigroup.add_mem' zero_mem'
mem_carrier 📖	mathematical	—	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.toSubsemigroup toSubmonoid Subsemiring SetLike.instMembership instSetLike	—	—
mem_inf 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike instMin	—	—
mem_mk 📖	mathematical	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.toSubsemigroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddZero.toZero	Subsemiring SetLike.instMembership instSetLike Submonoid Submonoid.instSetLike	—	—
mem_mk' 📖	mathematical	SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike AddSubmonoid AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoid.instSetLike	Subsemiring SetLike.instMembership instSetLike mk' Set Set.instMembership	—	—
mem_toAddSubmonoid 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SetLike.instMembership AddSubmonoid.instSetLike toAddSubmonoid Subsemiring instSetLike	—	—
mem_toNonUnitalSubsemiring 📖	mathematical	—	NonUnitalSubsemiring NonAssocSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalSubsemiring.instSetLike toNonUnitalSubsemiring Subsemiring instSetLike	—	—
mem_toSubmonoid 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass SetLike.instMembership Submonoid.instSetLike toSubmonoid Subsemiring instSetLike	—	—
mem_top 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike Top.top instTop	—	Set.mem_univ
mk'_toAddSubmonoid 📖	mathematical	SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike AddSubmonoid AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoid.instSetLike	toAddSubmonoid mk'	—	SetLike.coe_injective
mk'_toSubmonoid 📖	mathematical	SetLike.coe Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.instSetLike AddSubmonoid AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddSubmonoid.instSetLike	toSubmonoid mk'	—	SetLike.coe_injective
mul_mem 📖	mathematical	Subsemiring SetLike.instMembership instSetLike	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass instSubsemiringClass
noZeroDivisors 📖	mathematical	—	NoZeroDivisors Subsemiring SetLike.instMembership instSetLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring toNonAssocSemiring ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne SubsemiringClass.toAddSubmonoidClass instSubsemiringClass	—	AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass instSubsemiringClass NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
nontrivial 📖	mathematical	—	Nontrivial Subsemiring SetLike.instMembership instSetLike	—	nontrivial_of_ne AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass instSubsemiringClass AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass zero_ne_one NeZero.one
nsmul_mem 📖	mathematical	Subsemiring SetLike.instMembership instSetLike	AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	nsmul_mem SubsemiringClass.toAddSubmonoidClass instSubsemiringClass
one_mem 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	OneMemClass.one_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass instSubsemiringClass
one_mem_toNonUnitalSubsemiring 📖	mathematical	—	NonUnitalSubsemiring NonAssocSemiring.toNonUnitalNonAssocSemiring SetLike.instMembership NonUnitalSubsemiring.instSetLike toNonUnitalSubsemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Submonoid.one_mem
pow_mem 📖	mathematical	Subsemiring Semiring.toNonAssocSemiring SetLike.instMembership instSetLike	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	pow_mem SubsemiringClass.toSubmonoidClass instSubsemiringClass
subtype_apply 📖	mathematical	—	DFunLike.coe RingHom Subsemiring SetLike.instMembership instSetLike toNonAssocSemiring RingHom.instFunLike subtype	—	—
subtype_injective 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike DFunLike.coe RingHom toNonAssocSemiring RingHom.instFunLike subtype	—	Subtype.coe_injective
toAddSubmonoid_injective 📖	mathematical	—	Subsemiring AddSubmonoid AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne toAddSubmonoid	—	ext SetLike.ext_iff
toNonUnitalSubsemiring_inj 📖	mathematical	—	toNonUnitalSubsemiring	—	toNonUnitalSubsemiring_injective
toNonUnitalSubsemiring_injective 📖	mathematical	—	Subsemiring NonUnitalSubsemiring NonAssocSemiring.toNonUnitalNonAssocSemiring toNonUnitalSubsemiring	—	SetLike.ext'_iff
toNonUnitalSubsemiring_toSubsemiring 📖	mathematical	—	NonUnitalSubsemiring.toSubsemiring toNonUnitalSubsemiring one_mem	—	one_mem
toSubmonoid_injective 📖	mathematical	—	Subsemiring Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass toSubmonoid	—	ext SetLike.ext_iff
zero_mem 📖	mathematical	—	Subsemiring SetLike.instMembership instSetLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass instSubsemiringClass
zero_mem' 📖	mathematical	—	Set Set.instMembership Subsemigroup.carrier MulOne.toMul MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Submonoid.toSubsemigroup toSubmonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—

SubsemiringClass

Definitions

Name	Category	Theorems
subtype 📖	CompOp	5 math math: RingHom.comp_restrict, RingHom.rangeS_codRestrict, subtype_injective, coe_subtype, subtype_apply
toCommSemiring 📖	CompOp	155 math math: LocalSubring.isLocalRing, ValuationSubring.coe_mem_principalUnitGroup_iff, ValuationSubring.valuation_lt_one_iff, ValuationSubring.image_maximalIdeal, ValuationSubring.integralClosure_algebraMap_injective, Valuation.mem_maximalIdeal_iff, IntermediateField.algHomEquivAlgHomOfSplits_apply_apply, NumberField.IsCMField.zpowers_complexConj_eq_top, IntermediateField.coe_algebraMap_over_bot, Algebra.algebraMap_ofSubsemiring_apply, NumberField.IsCMField.equivInfinitePlace_symm_apply, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Valuation.HasExtension.instIsLocalHomSubtypeMemValuationSubringValuationSubringRingHomAlgebraMap, NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, Polynomial.int_coeff_eq, Algebra.coe_algebraMap_ofSubring, ValuationSubring.ofPrime_valuation_eq_one_iff_mem_primeCompl, ValuationSubring.valuation_unit, Subfield.relfinrank_eq_finrank_of_le, isLocalRing_top, Algebra.toSubring_bot, IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, ValuationSubring.subtype_injective, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', Algebra.coe_algebraMap_ofSubsemiring, IntermediateField.LinearDisjoint.trace_algebraMap, NumberField.IsCMField.isQuadraticExtension, Valuation.leIdeal_map_algebraMap_eq_leSubmodule_min, NumberField.IsCMField.orderOf_complexConj, ValuationSubring.isLocalRing, IntermediateField.restrictRestrictAlgEquivMapHom_apply, ValuationSubring.idealOfLE_le_of_le, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, normalClosure.restrictScalars_eq, Ideal.image_subset_nonunits_valuationSubring, IntermediateField.LinearDisjoint.basisOfBasisLeft_apply, algebraicClosure.isIntegralClosure, is_noetherian_subring_closure, NumberField.IsCMField.complexConj_apply_apply, Valuation.HasExtension.maximalIdeal_comap_algebraMap_eq_maximalIdeal, IntermediateField.LinearDisjoint.basisOfBasisRight_apply, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, NumberField.IsCMField.coe_ringOfIntegersComplexConj, ValuationSubring.primeSpectrumOrderEquiv_apply_coe_carrier, Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, IntermediateField.botContinuousSMul, NumberField.IsCMField.equivInfinitePlace_apply, LocalSubring.instAtPrimeSubtypeMemSubringToSubringOfPrime, ValuationSubring.coe_unitGroupMulEquiv_apply, NumberField.IsCMField.is_quadratic, Valuation.pow_Uniformizer_is_pow_generator, NumberField.IsCMField.complexConj_apply_eq_self, IntermediateField.instIsScalarTowerSubtypeMemAdjoinSingletonSetCoeRingHomAlgebraMap, Subfield.algebraMap_ofSubfield, Valuation.ideal_isPrincipal, ValuationSubring.instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, Valuation.associated_of_isUniformizer, Submodule.traceDual_le_span_map_traceDual, IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, LocalSubring.map_maximalIdeal_eq_top_of_isMax, NumberField.IsCMField.complexEmbedding_complexConj, PadicInt.coe_adicCompletionIntegersEquiv_apply, Polynomial.int_eval₂_eq, ValuationSubring.instIsDomainSubtypeMem, IntermediateField.algebraMap_apply, IntermediateField.LinearDisjoint.norm_algebraMap, ValuationSubring.instIsFractionRingSubtypeMem, Valuation.HasExtension.instIsScalarTower_valuationSubring', Valuation.HasExtension.val_algebraMap, ValuationSubring.algebraMap_apply, ValuationSubring.valuation_eq_iff, Valuation.valuationSubring_isPrincipalIdealRing, IsLocalRing.exists_factor_valuationRing, Algebra.algebraMap_ofSubring, Valuation.HasExtension.instIsLocalHomValuationInteger, Valued.integer.coe_span_singleton_eq_closedBall, Polynomial.int_leadingCoeff_eq, Polynomial.map_restriction, ValuationSubring.coe_mem_nonunits_iff, ValuationSubring.mem_nonunits_iff_exists_mem_maximalIdeal, IntermediateField.AdjoinPair.algebraMap_gen₁, FixedPoints.toAlgAut_surjective, Polynomial.int_monic_iff, Valuation.HasExtension.instIsTorsionFreeInteger, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, Valued.integer.norm_unit, ValuationSubring.prime_idealOfLE, minpoly.ofSubring, ValuationSubring.ofPrime_scalar_tower, IsGaloisGroup.intermediateField, ValuationSubring.principalUnitGroupEquiv_apply, IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, spectralNorm.eq_of_normalClosure', Submodule.traceDual_eq_span_map_traceDual_of_linearDisjoint, Subfield.relrank_eq_rank_of_le, IntermediateField.isScalarTower_over_bot, Valuation.valuationSubring_not_isField, IntermediateField.adjoin_eq_range_algebraMap_adjoin, IntermediateField.exists_algHom_adjoin_of_splits', FixedPoints.toAlgHom_bijective, IsGaloisGroup.fixedPoints, ValuationSubring.coe_unitGroupMulEquiv_symm_apply, Valuation.Integer.not_isUnit_iff_valuation_lt_one, Valuation.exists_pow_Uniformizer, NumberField.IsCMField.complexConj_eq_self_iff, IsGaloisGroup.subgroup, Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, LocalSubring.instIsScalarTowerSubtypeMemSubringToSubringOfPrime, Valuation.HasExtension.mk_smul_mk, Valued.integer.isUnit_iff_norm_eq_one, Valuation.IsUniformizer.not_isUnit, Valued.integer.isPrincipalIdealRing_of_compactSpace, instIsLocalRingSubtypeMemSubringMapOfNontrivial, LocalSubring.le_def, NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, Valuation.IsUniformizer.is_generator, IntermediateField.adjoin_minpoly_coeff_of_exists_primitive_element, FixedPoints.toAlgAut_bijective, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply, Valuation.Uniformizer.is_generator, ValuationSubring.coe_primeSpectrumOrderEquiv_symm_apply_asIdeal, NumberField.IsCMField.infinitePlace_complexConj, ValuationSubring.subtype_apply, FixedPoints.coe_algebraMap, ValuationSubring.valuation_eq_one_iff, ValuationSubring.ofPrime_localization, Valuation.HasExtension.instIsScalarTower_valuationSubring, Algebra.algebraMap_ofSubring_apply, Valued.integer.norm_coe_unit, Valuation.HasExtension.coe_algebraMap_valuationSubring_eq, ValuationSubring.algebraMap_injective, Valuation.HasExtension.instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal, perfectClosure.perfectRing, Valuation.leSubmodule_comap_algebraMap_eq_leIdeal, instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, ValuationSubring.primeSpectrumEquiv_apply, NumberField.IsCMField.complexConj_torsion, ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, ValuationSubring.coe_subtype, Valuation.HasExtension.algebraMap_residue_eq_residue_algebraMap, IntermediateField.AdjoinPair.algebraMap_gen₂, NumberField.IsCMField.Units.complexConj_eq_self_iff, Polynomial.int_natDegree, IntermediateField.AdjoinSimple.algebraMap_gen, ValuationSubring.principalUnitGroup_symm_apply, Valuation.HasExtension.algebraMap_injective, ValuationRing.instIsFractionRingInteger, Valuation.HasExtension.algebraMap_mem_maximalIdeal_iff, Valuation.HasExtension.instIsScalarTowerInteger, Valuation.HasExtension.val_smul
toNonAssocSemiring 📖	CompOp	16 math math: RingHom.comp_restrict, RingEquiv.restrict_symm_apply_coe, RingHom.surjective_codRestrict, instIsStablyFiniteRingSubtypeMem, RingHom.rangeS_codRestrict, RingHom.injective_codRestrict, subtype_injective, coe_subtype, noZeroDivisors, IsLocalRing.exists_factor_valuationRing, RingEquiv.restrict_apply_coe, instCharZero, RingHom.codRestrict_apply, subtype_apply, RingHom.restrict_apply, RingHom.coe_restrict_apply
toSemiring 📖	CompOp	22 math math: StarAlgEquiv.ofInjective_symm_apply, StarSubalgebra.inclusion_apply, NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe, StarSubalgebra.subtype_comp_inclusion, StarAlgEquiv.ofInjective_apply, SubalgebraClass.coe_val, StarAlgHom.coe_codRestrict, StarSubalgebra.subtype_apply, StarSubalgebra.isClosedEmbedding_inclusion, StarSubalgebra.instIsTopologicalSemiringSubtypeMem, StarSubalgebra.coe_subtype, toIsOrderedRing, StarSubalgebra.starModule, SubalgebraClass.coe_algebraMap, StarSubalgebra.toSubalgebra_subtype, StarAlgHom.subtype_comp_codRestrict, StarSubalgebra.inclusion_injective, toIsStrictOrderedRing, cfcHom_eq_of_isStarNormal, StarAlgHom.injective_codRestrict, StarSubalgebra.isEmbedding_inclusion, continuousFunctionalCalculus_map_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addSubmonoidWithOneClass 📖	mathematical	—	AddSubmonoidWithOneClass AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	toAddSubmonoidClass SubmonoidClass.toOneMemClass toSubmonoidClass
coe_subtype 📖	mathematical	—	DFunLike.coe RingHom SetLike.instMembership toNonAssocSemiring RingHom.instFunLike subtype	—	—
noZeroDivisors 📖	mathematical	—	NoZeroDivisors SetLike.instMembership Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring toNonAssocSemiring ZeroMemClass.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne toAddSubmonoidClass	—	Function.Injective.noZeroDivisors AddSubmonoidClass.toZeroMemClass toAddSubmonoidClass Subtype.coe_injective
nonUnitalSubsemiringClass 📖	mathematical	—	NonUnitalSubsemiringClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	toAddSubmonoidClass MulMemClass.mul_mem SubmonoidClass.toMulMemClass toSubmonoidClass
nontrivial 📖	mathematical	—	Nontrivial SetLike.instMembership	—	nontrivial_of_ne AddSubmonoidClass.toZeroMemClass toAddSubmonoidClass AddSubmonoidWithOneClass.toOneMemClass addSubmonoidWithOneClass zero_ne_one NeZero.one
subtype_apply 📖	mathematical	—	DFunLike.coe RingHom SetLike.instMembership toNonAssocSemiring RingHom.instFunLike subtype	—	—
subtype_injective 📖	mathematical	—	SetLike.instMembership DFunLike.coe RingHom toNonAssocSemiring RingHom.instFunLike subtype	—	—
toAddSubmonoidClass 📖	mathematical	—	AddSubmonoidClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
toSubmonoidClass 📖	mathematical	—	SubmonoidClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass	—	—

(root)

Definitions

Name	Category	Theorems
AddSubmonoidWithOneClass 📖	CompData	1 math math: SubsemiringClass.addSubmonoidWithOneClass
SubsemiringClass 📖	CompData	8 math math: RingConeClass.toSubsemiringClass, StarSubalgebra.subsemiringClass, StarSubsemiring.subsemiringClass, Subsemiring.instSubsemiringClass, Subalgebra.instSubsemiringClass, HomogeneousSubsemiring.subsemiringClass, RingPreordering.instSubsemiringClass, SubringClass.toSubsemiringClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
natCast_mem 📖	mathematical	—	SetLike.instMembership AddMonoidWithOne.toNatCast	—	Nat.cast_zero AddSubmonoidClass.toZeroMemClass AddSubmonoidWithOneClass.toAddSubmonoidClass Nat.cast_add Nat.cast_one AddSubmonoidClass.toAddMemClass AddSubmonoidWithOneClass.toOneMemClass
ofNat_mem 📖	mathematical	—	SetLike.instMembership	—	Nat.cast_ofNat natCast_mem

---

← Back to Index