Filtration

📁 Source: Mathlib/RingTheory/Filtration.lean

Statistics

Metric	Count
Definitions Filtration, N, Stable, instBot, instCompleteLattice, instInfSet, instInhabited, instMax, instMin, instPartialOrder, instSupSet, instTop, submodule, submoduleInfHom, stableFiltration, trivialFiltration, Filtration	17
Theorems bounded_difference, exists_forall_le, exists_pow_smul_eq, exists_pow_smul_eq_of_ge, inter_left, inter_right, of_le, antitone, bot_N, ext, ext_iff, iInf_N, iSup_N, inf_N, inf_submodule, mem_submodule, mono, pow_smul_le, pow_smul_le_pow_smul, sInf_N, sSup_N, smul_le, stable_iff_exists_pow_smul_eq_of_ge, submodule_closure_single, submodule_eq_span_le_iff_stable_ge, submodule_fg_iff_stable, submodule_span_single, sup_N, top_N, exists_pow_inf_eq_pow_smul, iInf_pow_eq_bot_of_isDomain, iInf_pow_eq_bot_of_isLocalRing, iInf_pow_smul_eq_bot_of_isLocalRing, iInf_pow_smul_eq_bot_of_isTorsionFree, iInf_pow_smul_eq_bot_of_le_jacobson, iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing, mem_iInf_smul_pow_eq_bot_iff, stableFiltration_N, stableFiltration_stable, trivialFiltration_N	41
Total	58

Ideal

Definitions

Name	Category	Theorems
Filtration 📖	CompData	11 math math: Filtration.sSup_N, Filtration.inf_N, Filtration.top_N, Filtration.sInf_N, Filtration.iInf_N, Filtration.inf_submodule, Filtration.sup_N, Filtration.bot_N, Filtration.Stable.inter_right, Filtration.Stable.inter_left, Filtration.iSup_N
stableFiltration 📖	CompOp	2 math math: stableFiltration_stable, stableFiltration_N
trivialFiltration 📖	CompOp	1 math math: trivialFiltration_N

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_pow_inf_eq_pow_smul 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instMin Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id Top.top Submodule.instTop	—	Filtration.Stable.exists_pow_smul_eq_of_ge Filtration.Stable.inter_right stableFiltration_stable
iInf_pow_eq_bot_of_isDomain 📖	mathematical	—	iInf Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Bot.bot Submodule.instBot	—	IsScalarTower.right IsScalarTower.left mul_top instIsTwoSided_1 iInf_pow_smul_eq_bot_of_isTorsionFree instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors NoZeroDivisors.toNoZeroSMulDivisors IsDomain.to_noZeroDivisors Module.Finite.self
iInf_pow_eq_bot_of_isLocalRing 📖	mathematical	—	iInf Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.instInfSet NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Bot.bot Submodule.instBot	—	IsScalarTower.right IsScalarTower.left ext smul_eq_mul one_eq_top mul_one iInf_pow_smul_eq_bot_of_isLocalRing Module.Finite.self
iInf_pow_smul_eq_bot_of_isLocalRing 📖	mathematical	—	iInf Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id Top.top Submodule.instTop Bot.bot Submodule.instBot	—	iInf_pow_smul_eq_bot_of_le_jacobson LE.le.trans IsLocalRing.le_maximalIdeal IsLocalRing.maximalIdeal_le_jacobson
iInf_pow_smul_eq_bot_of_isTorsionFree 📖	mathematical	—	iInf Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id Top.top Submodule.instTop Bot.bot Submodule.instBot	—	IsScalarTower.left IsScalarTower.right eq_bot_iff mem_iInf_smul_pow_eq_bot_iff smul_left_injective IsDomain.toIsCancelMulZero one_smul Iff.not eq_top_iff_one Subtype.prop
iInf_pow_smul_eq_bot_of_le_jacobson 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule jacobson CommRing.toRing Bot.bot Ring.toSemiring Submodule.instBot	iInf Submodule AddCommGroup.toAddCommMonoid Submodule.instInfSet Submodule.instSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id Top.top Submodule.instTop	—	IsScalarTower.left IsScalarTower.right eq_bot_iff mem_iInf_smul_pow_eq_bot_iff isUnit_of_sub_one_mem_jacobson_bot sub_sub_cancel_left NonUnitalSubringClass.toNegMemClass instNonUnitalSubringClassIdeal IsUnit.smul_left_cancel sub_smul one_smul sub_self smul_zero
iInf_pow_smul_eq_bot_of_noZeroSMulDivisors 📖	mathematical	—	iInf Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id Top.top Submodule.instTop Bot.bot Submodule.instBot	—	iInf_pow_smul_eq_bot_of_isTorsionFree
isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing 📖	mathematical	—	IsIdempotentElem Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Top.top Submodule.instTop	—	IsScalarTower.right eq_bot_iff iInf_pow_eq_bot_of_isLocalRing le_iInf pow_zero one_eq_top IsIdempotentElem.pow_succ_eq Submodule.mul_bot mul_top instIsTwoSided_1
mem_iInf_smul_pow_eq_bot_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike iInf Submodule.instInfSet Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id Top.top Submodule.instTop SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	IsScalarTower.left IsScalarTower.right inf_eq_right LE.le.trans iInf_le le_of_eq Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul IsNoetherian.noetherian isNoetherian_of_isNoetherianRing_of_finite Filtration.Stable.inter_right stableFiltration_stable le_refl Submodule.mem_iInf pow_zero one_eq_top Submodule.top_smul add_comm pow_add smul_smul pow_one Submodule.smul_mem_smul Subtype.prop
stableFiltration_N 📖	mathematical	—	Filtration.N stableFiltration Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule AddCommGroup.toAddCommMonoid Submodule.instSMul Semiring.toModule Submodule.instPowNat	—	—
stableFiltration_stable 📖	mathematical	—	Filtration.Stable stableFiltration	—	add_comm pow_add IsScalarTower.right SemigroupAction.mul_smul pow_one
trivialFiltration_N 📖	mathematical	—	Filtration.N trivialFiltration	—	—

Ideal.Filtration

Definitions

Name	Category	Theorems
N 📖	CompOp	23 math math: submodule_closure_single, submodule_eq_span_le_iff_stable_ge, ext_iff, smul_le, mem_submodule, sSup_N, inf_N, top_N, sInf_N, iInf_N, Stable.exists_pow_smul_eq_of_ge, Stable.exists_pow_smul_eq, submodule_span_single, sup_N, antitone, stable_iff_exists_pow_smul_eq_of_ge, bot_N, pow_smul_le_pow_smul, Ideal.stableFiltration_N, pow_smul_le, mono, Ideal.trivialFiltration_N, iSup_N
Stable 📖	MathDef	3 math math: Ideal.stableFiltration_stable, stable_iff_exists_pow_smul_eq_of_ge, submodule_fg_iff_stable
instBot 📖	CompOp	1 math math: bot_N
instCompleteLattice 📖	CompOp	—
instInfSet 📖	CompOp	2 math math: sInf_N, iInf_N
instInhabited 📖	CompOp	—
instMax 📖	CompOp	1 math math: sup_N
instMin 📖	CompOp	4 math math: inf_N, inf_submodule, Stable.inter_right, Stable.inter_left
instPartialOrder 📖	CompOp	—
instSupSet 📖	CompOp	2 math math: sSup_N, iSup_N
instTop 📖	CompOp	1 math math: top_N
submodule 📖	CompOp	6 math math: submodule_closure_single, submodule_eq_span_le_iff_stable_ge, mem_submodule, inf_submodule, submodule_span_single, submodule_fg_iff_stable
submoduleInfHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone 📖	mathematical	—	Antitone Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Nat.instPreorder PartialOrder.toPreorder Submodule.instPartialOrder N	—	antitone_nat_of_succ_le mono
bot_N 📖	mathematical	—	N Bot.bot Ideal.Filtration instBot Pi.instBotForall Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instBot	—	—
ext 📖	—	N	—	—	IsScalarTower.left
ext_iff 📖	mathematical	—	N	—	ext
iInf_N 📖	mathematical	—	N iInf Ideal.Filtration instInfSet Pi.infSet Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet	—	Set.range_comp
iSup_N 📖	mathematical	—	N iSup Ideal.Filtration instSupSet Pi.supSet Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	Set.range_comp
inf_N 📖	mathematical	—	N Ideal.Filtration instMin Pi.instMinForall_mathlib Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instMin	—	—
inf_submodule 📖	mathematical	—	submodule Ideal.Filtration instMin Submodule Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Subalgebra Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id SetLike.instMembership Subalgebra.instSetLike reesAlgebra PolynomialModule Subalgebra.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule Subalgebra.moduleLeft PolynomialModule.polynomialModule Submodule.instMin	—	Submodule.ext
mem_submodule 📖	mathematical	—	PolynomialModule Submodule Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Subalgebra Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id SetLike.instMembership Subalgebra.instSetLike reesAlgebra Subalgebra.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule Subalgebra.moduleLeft PolynomialModule.polynomialModule Submodule.setLike submodule N DFunLike.coe Finsupp NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instFunLike	—	—
mono 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder N	—	—
pow_smul_le 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id N	—	IsScalarTower.left IsScalarTower.right pow_zero Ideal.one_eq_top Submodule.top_smul zero_add pow_succ' SemigroupAction.mul_smul add_assoc add_comm LE.le.trans smul_mono_right Submodule.instCovariantClassHSMulLe_1 smul_le
pow_smul_le_pow_smul 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id N	—	IsScalarTower.left IsScalarTower.right add_comm pow_add SemigroupAction.mul_smul smul_mono_right Submodule.instCovariantClassHSMulLe_1 pow_smul_le
sInf_N 📖	mathematical	—	N InfSet.sInf Ideal.Filtration instInfSet Pi.infSet Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet Set.image	—	—
sSup_N 📖	mathematical	—	N SupSet.sSup Ideal.Filtration instSupSet Pi.supSet Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set.image	—	—
smul_le 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction N	—	—
stable_iff_exists_pow_smul_eq_of_ge 📖	mathematical	—	Stable N Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule AddCommGroup.toAddCommMonoid Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id	—	IsScalarTower.left IsScalarTower.right Stable.exists_pow_smul_eq_of_ge smul_smul pow_succ' tsub_add_eq_add_tsub CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
submodule_closure_single 📖	mathematical	—	AddSubmonoid.closure PolynomialModule AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupPolynomialModule Set.iUnion Set.image DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoidHom.instFunLike PolynomialModule.single SetLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.setLike N Submodule.toAddSubmonoid Polynomial Subalgebra Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id SetLike.instMembership Subalgebra.instSetLike reesAlgebra Subalgebra.toSemiring Subalgebra.moduleLeft PolynomialModule.polynomialModule submodule	—	le_antisymm AddSubmonoid.closure_le Set.iUnion_subset_iff PolynomialModule.single_apply Submodule.zero_mem Finsupp.sum_single AddSubmonoid.sum_mem AddSubmonoid.subset_closure Set.subset_iUnion Set.mem_image_of_mem
submodule_eq_span_le_iff_stable_ge 📖	mathematical	—	submodule Submodule.span Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Subalgebra Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id SetLike.instMembership Subalgebra.instSetLike reesAlgebra PolynomialModule Subalgebra.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule Subalgebra.moduleLeft PolynomialModule.polynomialModule Set.iUnion Set.image DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike PolynomialModule.single SetLike.coe Submodule Submodule.setLike N Ideal Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	IsScalarTower.left submodule_span_single LE.le.ge_iff_eq' Submodule.span_mono Set.iUnion₂_subset_iUnion Submodule.span_le Set.iUnion_subset_iff LE.le.antisymm smul_le Finsupp.mem_span_iff_linearCombination PolynomialModule.single_apply Finsupp.linearCombination_apply Finsupp.sum_apply Submodule.sum_mem Subalgebra.smul_def PolynomialModule.smul_single_apply IsScalarTower.right pow_smul_le_pow_smul add_comm add_tsub_assoc_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le pow_one tsub_add_cancel_of_le Submodule.smul_mem_smul HasSubset.Subset.trans Set.instIsTransSubset Set.subset_iUnion₂ Submodule.subset_span zero_le Submodule.smul_induction_on PolynomialModule.monomial_smul_single Submodule.smul_mem reesAlgebra.monomial_mem Set.mem_image_of_mem map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass Submodule.add_mem
submodule_fg_iff_stable 📖	mathematical	Submodule.FG CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid N	Polynomial Subalgebra Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id SetLike.instMembership Subalgebra.instSetLike reesAlgebra PolynomialModule Subalgebra.toSemiring instAddCommGroupPolynomialModule Subalgebra.moduleLeft PolynomialModule.polynomialModule submodule Stable	—	IsScalarTower.left submodule_eq_span_le_iff_stable_ge Submodule.FG.stabilizes_of_iSup_eq Submodule.span_le Set.iUnion₂_subset_iff Set.Subset.trans Set.subset_iUnion₂ LE.le.trans Submodule.subset_span Submodule.span_iUnion submodule_span_single Set.ext le_refl Submodule.span_iUnion₂ iSup_congr_Prop iSup_subtype' Submodule.fg_iSup Finite.of_fintype Finset.coe_image Submodule.span_span_of_tower Subalgebra.isScalarTower_mid Polynomial.isScalarTower IsScalarTower.right PolynomialModule.isScalarTower' RingHomSurjective.ids Submodule.map_span
submodule_span_single 📖	mathematical	—	Submodule.span Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Subalgebra Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id SetLike.instMembership Subalgebra.instSetLike reesAlgebra PolynomialModule Subalgebra.toSemiring AddCommGroup.toAddCommMonoid instAddCommGroupPolynomialModule Subalgebra.moduleLeft PolynomialModule.polynomialModule Set.iUnion Set.image DFunLike.coe AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike PolynomialModule.single SetLike.coe Submodule Submodule.setLike N submodule	—	Submodule.span_closure submodule_closure_single Submodule.coe_toAddSubmonoid Submodule.span_eq
sup_N 📖	mathematical	—	N Ideal.Filtration instMax Pi.instMaxForall_mathlib Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	—	—
top_N 📖	mathematical	—	N Top.top Ideal.Filtration instTop Pi.instTopForall Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instTop	—	—

Ideal.Filtration.Stable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bounded_difference 📖	mathematical	Ideal.Filtration.Stable Ideal.Filtration.N	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	—	exists_forall_le le_of_eq LE.le.trans Ideal.Filtration.antitone IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
exists_forall_le 📖	—	Ideal.Filtration.Stable Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Ideal.Filtration.N	—	—	LE.le.trans Ideal.Filtration.antitone zero_add Nat.instCanonicallyOrderedAdd add_right_comm covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le smul_mono_right Submodule.instCovariantClassHSMulLe_1 Ideal.Filtration.smul_le
exists_pow_smul_eq 📖	mathematical	Ideal.Filtration.Stable	Ideal.Filtration.N Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule AddCommGroup.toAddCommMonoid Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id	—	IsScalarTower.left IsScalarTower.right add_zero pow_zero Ideal.one_eq_top Submodule.top_smul add_assoc add_comm pow_add SemigroupAction.mul_smul pow_one
exists_pow_smul_eq_of_ge 📖	mathematical	Ideal.Filtration.Stable	Ideal.Filtration.N Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule AddCommGroup.toAddCommMonoid Submodule.instSMul Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Submodule.instPowNat IsScalarTower.right Algebra.id	—	IsScalarTower.left IsScalarTower.right exists_pow_smul_eq add_comm tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub
inter_left 📖	mathematical	Ideal.Filtration.Stable	Ideal.Filtration Ideal.Filtration.instMin	—	of_le inf_le_right
inter_right 📖	mathematical	Ideal.Filtration.Stable	Ideal.Filtration Ideal.Filtration.instMin	—	of_le inf_le_left
of_le 📖	—	Ideal.Filtration.Stable Ideal.Filtration Preorder.toLE PartialOrder.toPreorder Ideal.Filtration.instPartialOrder	—	—	Ideal.Filtration.submodule_fg_iff_stable IsNoetherian.noetherian isNoetherian_of_isNoetherianRing_of_finite isNoetherian_of_fg_of_noetherian instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra isNoetherian_submodule OrderHomClass.mono InfHomClass.toOrderHomClass InfHom.instInfHomClass

MeasureTheory

Definitions

Name	Category	Theorems
Filtration 📖	CompData	6 math math: Filtration.coeFn_sup, Filtration.le_rightCont, Filtration.sSup_def, Filtration.IsRightContinuous.RC, Filtration.coeFn_inf, Filtration.sInf_def

---

← Back to Index