Documentation Verification Report

SubDPIdeal

📁 Source: Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean

Statistics

Metric	Count
Definitions `ker`, `IsSubDPIdeal`, `dividedPowers`, `dividedPowers`, `dpow`, `dividedPowers`, `dpow`, `SubDPIdeal`, `carrier`, `inhabited`, `instBot`, `instCoeOutElemIdealIic`, `instCoeOutIdeal`, `instCompleteLattice`, `instInfSet`, `instLE`, `instLT`, `instMax`, `instMin`, `instPartialOrder`, `instSetLike`, `instSupSet`, `instTop`, `mk'`, `prod`, `span`, `toIdeal`, `dpEqualizer`, `subDPIdeal_inf_of_quot`	29
Theorems `dpow_eq`, `dpow_eq_of_mem`, `dpow_mem`, `isDPMorphism`, `isSubideal`, `self`, `dividedPowers_unique`, `dpow_apply`, `dpow_apply'`, `dpow_def`, `isDPMorphism`, `dividedPowers_unique`, `dpow_apply`, `isDPMorphism`, `coe_def`, `dpow_mem`, `dpow_mem_span_of_mem_span`, `ext`, `ext_iff`, `inf_carrier_def`, `isSubideal`, `le_iff`, `lt_iff`, `memCarrier`, `sInf_carrier_def`, `sSup_carrier_def`, `span_carrier_eq_dpow_span`, `sup_carrier_def`, `toIsSubDPIdeal`, `dpEqualizer_is_dp_ideal_left`, `dpEqualizer_is_dp_ideal_right`, `dpow_span_isSubideal`, `isSubDPIdeal_iInf`, `isSubDPIdeal_iSup`, `isSubDPIdeal_inf_iff`, `isSubDPIdeal_ker`, `isSubDPIdeal_map`, `isSubDPIdeal_map_of_isSubDPIdeal`, `isSubDPIdeal_sup`, `le_equalizer_of_isDPMorphism`, `mem_dpEqualizer_iff`, `span_isSubDPIdeal_iff`	42
Total	71

DividedPowers

Definitions

Name	Category	Theorems
`IsSubDPIdeal` 📖	CompData	8 math math: `isSubDPIdeal_map`, `dpEqualizer_is_dp_ideal_left`, `isSubDPIdeal_ker`, `span_isSubDPIdeal_iff`, `dpEqualizer_is_dp_ideal_right`, `isSubDPIdeal_inf_iff`, `IsSubDPIdeal.self`, `SubDPIdeal.toIsSubDPIdeal`
`SubDPIdeal` 📖	CompData	7 math math: `SubDPIdeal.sInf_carrier_def`, `SubDPIdeal.le_iff`, `SubDPIdeal.inf_carrier_def`, `SubDPIdeal.sSup_carrier_def`, `SubDPIdeal.memCarrier`, `SubDPIdeal.sup_carrier_def`, `SubDPIdeal.lt_iff`
`dpEqualizer` 📖	CompOp	4 math math: `mem_dpEqualizer_iff`, `dpEqualizer_is_dp_ideal_left`, `le_equalizer_of_isDPMorphism`, `dpEqualizer_is_dp_ideal_right`
`subDPIdeal_inf_of_quot` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dpEqualizer_is_dp_ideal_left` 📖	mathematical	—	`IsSubDPIdeal` `dpEqualizer`	—	`dpow_mem` `dpow_comp`
`dpEqualizer_is_dp_ideal_right` 📖	mathematical	—	`IsSubDPIdeal` `dpEqualizer`	—	`dpow_mem` `dpow_comp`
`dpow_span_isSubideal` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Ideal.span` `setOf` `Set.instMembership` `dpow`	—	`Ideal.span_le` `dpow_mem`
`isSubDPIdeal_iInf` 📖	mathematical	`IsSubDPIdeal`	`Ideal` `CommSemiring.toSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `iInf` `Submodule.instInfSet`	—	`isEmpty_or_nonempty` `iInf_of_empty` `inf_of_le_left` `IsSubDPIdeal.self` `dpow_mem` `IsSubDPIdeal.dpow_mem`
`isSubDPIdeal_iSup` 📖	mathematical	`IsSubDPIdeal`	`iSup` `Ideal` `CommSemiring.toSemiring` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Ideal.iSup_eq_span` `span_isSubDPIdeal_iff` `Set.iUnion_subset_iff` `IsSubDPIdeal.isSubideal` `Ideal.span_mono` `Set.subset_iUnion` `Ideal.subset_span` `IsSubDPIdeal.dpow_mem`
`isSubDPIdeal_inf_iff` 📖	mathematical	—	`IsSubDPIdeal` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `dpow`	—	`Ideal.sub_mem` `add_sub_cancel` `dpow_add'` `Finset.range_add_one` `Finset.sum_insert` `Finset.notMem_range_self` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `dpow_zero` `mul_one` `add_sub_cancel_left` `Submodule.sum_mem` `SemilatticeInf.inf_le_left` `Submodule.smul_mem` `IsSubDPIdeal.dpow_mem` `ne_of_gt` `Finset.mem_range` `SemilatticeInf.inf_le_right` `sub_zero` `dpow_eval_zero` `Ideal.zero_mem` `dpow_mem`
`isSubDPIdeal_ker` 📖	mathematical	`IsDPMorphism` `CommRing.toCommSemiring`	`IsSubDPIdeal` `Ideal` `CommSemiring.toSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass`	—	`RingHom.instRingHomClass` `isSubDPIdeal_inf_iff`
`isSubDPIdeal_map` 📖	mathematical	`IsDPMorphism`	`IsSubDPIdeal` `Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	—	`isSubDPIdeal_map_of_isSubDPIdeal` `IsSubDPIdeal.self`
`isSubDPIdeal_map_of_isSubDPIdeal` 📖	mathematical	`IsDPMorphism` `IsSubDPIdeal`	`Ideal.map` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike`	—	`Ideal.map.eq_1` `span_isSubDPIdeal_iff` `IsDPMorphism.ideal_comp` `Ideal.mem_map_of_mem` `IsSubDPIdeal.isSubideal` `IsSubDPIdeal.dpow_mem` `IsDPMorphism.dpow_comp`
`isSubDPIdeal_sup` 📖	mathematical	`IsSubDPIdeal`	`Ideal` `CommSemiring.toSemiring` `SemilatticeSup.toMax` `IdemSemiring.toSemilatticeSup` `Submodule.idemSemiring` `Algebra.id`	—	`Ideal.span_eq` `Ideal.span_union` `span_isSubDPIdeal_iff` `Set.union_subset_iff` `IsSubDPIdeal.isSubideal` `Ideal.span_mono` `Set.subset_union_left` `Ideal.subset_span` `IsSubDPIdeal.dpow_mem` `Set.subset_union_right`
`le_equalizer_of_isDPMorphism` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.map` `RingHom` `RingHom.instFunLike` `IsDPMorphism`	`dpEqualizer`	—	`Ideal.map.eq_1` `Ideal.span_le` `Ideal.mem_map_of_mem` `IsDPMorphism.dpow_comp`
`mem_dpEqualizer_iff` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `dpEqualizer` `dpow`	—	—
`span_isSubDPIdeal_iff` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`IsSubDPIdeal` `Ideal.span` `SetLike.instMembership` `dpow`	—	`IsSubDPIdeal.dpow_mem` `Ideal.subset_span` `Ideal.span_le` `Submodule.span_induction` `dpow_eval_zero` `Ideal.zero_mem` `dpow_add'` `Submodule.sum_mem` `Ideal.mul_mem_left` `Ideal.mul_mem_right` `Ideal.instIsTwoSided` `smul_eq_mul` `dpow_mul`

DividedPowers.DPMorphism

Definitions

Name	Category	Theorems
`ker` 📖	CompOp	—

DividedPowers.IsSubDPIdeal

Definitions

Name	Category	Theorems
`dividedPowers` 📖	CompOp	3 math math: `dpow_eq_of_mem`, `isDPMorphism`, `dpow_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dpow_eq` 📖	mathematical	`DividedPowers.IsSubDPIdeal`	`DividedPowers.dpow` `dividedPowers` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`dpow_eq_of_mem` 📖	mathematical	`DividedPowers.IsSubDPIdeal` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DividedPowers.dpow` `dividedPowers`	—	`dpow_eq`
`dpow_mem` 📖	mathematical	`DividedPowers.IsSubDPIdeal` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DividedPowers.dpow`	—	—
`isDPMorphism` 📖	mathematical	`DividedPowers.IsSubDPIdeal`	`DividedPowers.IsDPMorphism` `dividedPowers` `RingHom.id` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`Ideal.map_id` `isSubideal` `dpow_eq_of_mem`
`isSubideal` 📖	mathematical	`DividedPowers.IsSubDPIdeal`	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`self` 📖	mathematical	—	`DividedPowers.IsSubDPIdeal`	—	`le_rfl` `DividedPowers.dpow_mem`

DividedPowers.Quotient

Definitions

Name	Category	Theorems
`dividedPowers` 📖	CompOp	3 math math: `isDPMorphism`, `dpow_apply`, `dividedPowers_unique`
`dpow` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dividedPowers_unique` 📖	mathematical	`DividedPowers.IsSubDPIdeal` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DividedPowers.IsDPMorphism` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.commSemiring` `Ideal.map` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike`	`dividedPowers`	—	`Ideal.instIsTwoSided_1` `OfSurjective.dividedPowers_unique` `Ideal.Quotient.mk_surjective` `refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv`
`dpow_apply` 📖	mathematical	`DividedPowers.IsSubDPIdeal` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike`	`DividedPowers.dpow` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.commSemiring` `Ideal.map` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `dividedPowers` `DFunLike.coe`	—	`OfSurjective.dpow_apply` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv`
`isDPMorphism` 📖	mathematical	`DividedPowers.IsSubDPIdeal` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DividedPowers.IsDPMorphism` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.commSemiring` `Ideal.map` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `dividedPowers`	—	`OfSurjective.isDPMorphism` `Ideal.instIsTwoSided_1` `Ideal.Quotient.mk_surjective` `refl` `IsPreorder.toRefl` `IsEquiv.toIsPreorder` `eq_isEquiv`

DividedPowers.Quotient.OfSurjective

Definitions

Name	Category	Theorems
`dividedPowers` 📖	CompOp	4 math math: `dpow_def`, `isDPMorphism`, `dividedPowers_unique`, `dpow_apply`
`dpow` 📖	CompOp	2 math math: `dpow_def`, `dpow_apply'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dividedPowers_unique` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ideal.map` `DividedPowers.IsSubDPIdeal` `Ideal` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom.instRingHomClass` `DividedPowers.IsDPMorphism`	`dividedPowers`	—	`RingHom.instRingHomClass` `DividedPowers.ext` `Ideal.mem_map_iff_of_surjective` `DividedPowers.IsDPMorphism.dpow_comp` `dpow_apply`
`dpow_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ideal.map` `DividedPowers.IsSubDPIdeal` `Ideal` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom.instRingHomClass` `SetLike.instMembership` `Submodule.setLike`	`DividedPowers.dpow` `dividedPowers`	—	`RingHom.instRingHomClass` `dpow_def` `dpow_apply'`
`dpow_apply'` 📖	mathematical	`DividedPowers.IsSubDPIdeal` `CommRing.toCommSemiring` `Ideal` `CommSemiring.toSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom` `RingHom.instFunLike` `RingHom.instRingHomClass` `SetLike.instMembership` `Submodule.setLike`	`dpow` `DFunLike.coe` `DividedPowers.dpow`	—	`RingHom.instRingHomClass` `Function.extend_def` `sub_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.mem_ker` `DividedPowers.isSubDPIdeal_inf_iff` `Submodule.coe_mem`
`dpow_def` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ideal.map` `DividedPowers.IsSubDPIdeal` `Ideal` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom.instRingHomClass`	`DividedPowers.dpow` `dividedPowers` `dpow`	—	`RingHom.instRingHomClass`
`isDPMorphism` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `Ideal.map` `DividedPowers.IsSubDPIdeal` `Ideal` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `RingHom.instRingHomClass`	`DividedPowers.IsDPMorphism` `dividedPowers`	—	`RingHom.instRingHomClass` `le_of_eq` `dpow_apply`

DividedPowers.SubDPIdeal

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	12 math math: `sInf_carrier_def`, `le_iff`, `ext_iff`, `isSubideal`, `inf_carrier_def`, `sSup_carrier_def`, `memCarrier`, `span_carrier_eq_dpow_span`, `sup_carrier_def`, `lt_iff`, `coe_def`, `toIsSubDPIdeal`
`inhabited` 📖	CompOp	—
`instBot` 📖	CompOp	—
`instCoeOutElemIdealIic` 📖	CompOp	—
`instCoeOutIdeal` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	—
`instInfSet` 📖	CompOp	1 math math: `sInf_carrier_def`
`instLE` 📖	CompOp	1 math math: `le_iff`
`instLT` 📖	CompOp	1 math math: `lt_iff`
`instMax` 📖	CompOp	1 math math: `sup_carrier_def`
`instMin` 📖	CompOp	1 math math: `inf_carrier_def`
`instPartialOrder` 📖	CompOp	—
`instSetLike` 📖	CompOp	1 math math: `memCarrier`
`instSupSet` 📖	CompOp	1 math math: `sSup_carrier_def`
`instTop` 📖	CompOp	1 math math: `sInf_carrier_def`
`mk'` 📖	CompOp	—
`prod` 📖	CompOp	—
`span` 📖	CompOp	1 math math: `span_carrier_eq_dpow_span`
`toIdeal` 📖	CompOp	2 math math: `sSup_carrier_def`, `coe_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_def` 📖	mathematical	—	`toIdeal` `carrier`	—	—
`dpow_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `carrier`	`DividedPowers.dpow`	—	—
`dpow_mem_span_of_mem_span` 📖	—	`Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.instMembership` `Ideal.span` `setOf` `Set.instMembership` `DividedPowers.dpow`	—	—	`DividedPowers.dpow_span_isSubideal` `Submodule.span_induction` `DividedPowers.dpow_comp` `Ideal.mul_mem_left` `Ideal.subset_span` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `DividedPowers.dpow_eval_zero` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `DividedPowers.dpow_add'` `Submodule.sum_mem` `Ideal.mul_mem_right` `Ideal.instIsTwoSided` `smul_eq_mul` `DividedPowers.dpow_mul`
`ext` 📖	—	`carrier`	—	—	—
`ext_iff` 📖	mathematical	—	`carrier`	—	`ext`
`inf_carrier_def` 📖	mathematical	—	`carrier` `DividedPowers.SubDPIdeal` `instMin` `Ideal` `CommSemiring.toSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`isSubideal` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `carrier`	—	—
`le_iff` 📖	mathematical	—	`DividedPowers.SubDPIdeal` `instLE` `Ideal` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `carrier`	—	—
`lt_iff` 📖	mathematical	—	`DividedPowers.SubDPIdeal` `instLT` `Ideal` `CommSemiring.toSemiring` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `carrier`	—	—
`memCarrier` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `carrier` `DividedPowers.SubDPIdeal` `instSetLike`	—	—
`sInf_carrier_def` 📖	mathematical	—	`carrier` `InfSet.sInf` `DividedPowers.SubDPIdeal` `instInfSet` `iInf` `Ideal` `CommSemiring.toSemiring` `Submodule.instInfSet` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set` `Set.instMembership` `Set.instInsert` `Top.top` `instTop`	—	—
`sSup_carrier_def` 📖	mathematical	—	`carrier` `SupSet.sSup` `DividedPowers.SubDPIdeal` `instSupSet` `Ideal` `CommSemiring.toSemiring` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Set.image` `toIdeal`	—	—
`span_carrier_eq_dpow_span` 📖	mathematical	`Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`carrier` `span` `Ideal.span` `setOf` `Set.instMembership` `DividedPowers.dpow`	—	`DividedPowers.dpow_span_isSubideal` `dpow_mem_span_of_mem_span` `le_antisymm` `Set.mem_insert_of_mem` `Ideal.subset_span` `one_ne_zero` `DividedPowers.dpow_one` `sInf_le_of_le` `iInf_congr_Prop` `ciInf_pos` `le_refl` `le_iInf₂_iff` `Ideal.span_le` `dpow_mem`
`sup_carrier_def` 📖	mathematical	—	`carrier` `DividedPowers.SubDPIdeal` `instMax` `Ideal` `CommSemiring.toSemiring` `Set` `Set.instMembership` `Set.Iic` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `isSubideal`	—	—
`toIsSubDPIdeal` 📖	mathematical	—	`DividedPowers.IsSubDPIdeal` `carrier`	—	`isSubideal` `dpow_mem`

---

← Back to Index