Defs

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

Statistics

Metric	Count
Definitions IsNoetherian, IsNoetherianRing	2
Theorems of_isNoetherianRing, fg_of_isNoetherianRing, noetherian, wellFoundedGT, wf, eventually_iSup_ker_pow_eq, eventually_disjoint_ker_pow_range_pow, isNoetherianRing_iff, isNoetherianRing_iff_ideal_fg, isNoetherian_def, isNoetherian_iff, isNoetherian_iff', isNoetherian_iff_fg_wellFounded, isNoetherian_mk, isNoetherian_of_le, isNoetherian_submodule, isNoetherian_submodule', isNoetherian_submodule_left, isNoetherian_submodule_right, monotone_stabilizes_iff_noetherian, set_has_maximal_iff_noetherian, wellFoundedGT	22
Total	24

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fg_of_isNoetherianRing 📖	mathematical	—	FG	—	IsNoetherian.noetherian

Ideal.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isNoetherianRing 📖	mathematical	—	Ideal.FG	—	Ideal.fg_of_isNoetherianRing

IsNoetherian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
noetherian 📖	mathematical	—	Submodule.FG	—	—
wellFoundedGT 📖	mathematical	—	WellFoundedGT Submodule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder	—	isNoetherian_iff'
wf 📖	mathematical	—	Submodule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder	—	isNoetherian_iff

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_iSup_ker_pow_eq 📖	mathematical	—	Filter.Eventually Submodule iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice ker RingHom.id Semiring.toNonAssocSemiring LinearMap Monoid.toNatPow Module.End.instMonoid Filter.atTop Nat.instPreorder	—	monotone_stabilizes_iff_noetherian Filter.eventually_atTop SemilatticeSup.instIsDirectedOrder le_antisymm iSup_le le_or_gt LE.le.trans le_refl OrderHom.monotone LT.lt.le le_iSup

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_disjoint_ker_pow_range_pow 📖	mathematical	—	Filter.Eventually Disjoint Submodule Submodule.instPartialOrder Submodule.instOrderBot LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Module.End LinearMap Monoid.toNatPow instMonoid LinearMap.range RingHomSurjective.ids Filter.atTop Nat.instPreorder	—	RingHomSurjective.ids monotone_stabilizes_iff_noetherian Filter.eventually_atTop SemilatticeSup.instIsDirectedOrder disjoint_iff Submodule.eq_bot_iff pow_map_zero_of_le pow_apply

(root)

Definitions

Name	Category	Theorems
IsNoetherian 📖	CompData	65 math math: isNoetherian_iff', LieDerivation.instNoetherian, isNoetherian_submodule_right, IsNoetherian.iff_rank_lt_aleph0, isNoetherian_mk, QuotientMapQuotient.isNoetherian, FractionalIdeal.isNoetherian_coeIdeal, isNoetherian_of_injective, isNoetherian_submodule, isNoetherian_of_le, LinearEquiv.isNoetherian_iff, isNoetherian_prod, isNoetherian_of_finite, isNoetherian_linearMap_pi, isNoetherian_iff_submodule_quotient, NumberField.RingOfIntegers.instIsNoetherianInt, isNoetherian_of_subsingleton, isNoetherian_adjoin_finset, isNoetherian_iff_fg_wellFounded, LinearMap.isNoetherian_iff_of_bijective, isNoetherianRing_iff, isNoetherian_linearMap, FractionalIdeal.isNoetherian_spanSingleton_inv_to_map_mul, isNoetherian_of_liesOver, IsSemisimpleModule.finite_tfae, isNoetherian_of_surjective, FractionalIdeal.isNoetherian_zero, isNoetherian_submodule', isNoetherian_quotient, isNoetherian_of_range_eq_ker, IsSemiprimaryRing.isNoetherian_iff_finite_of_jacobson_fg, IsNoetherian.iff_fg, isNoetherian_def, monotone_stabilizes_iff_noetherian, isNoetherian_of_finite_isArtinian, isNoetherian_of_tower, IsDedekindRing.toIsNoetherian, Nat.instIsNoetherian, NumberField.RingOfIntegers.extension_isNoetherian, FractionalIdeal.isNoetherian_iff, IsArtinianRing.tfae, LieSubalgebra.instIsNoetherianSubtypeMem, isNoetherian_of_fg_of_noetherian, isNoetherian_span_of_finite, FunctionField.ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc, isNoetherian_submodule_left, IsDedekindDomainDvr.toIsNoetherian, IsSemiprimaryRing.isNoetherian_iff_isArtinian, FractionalIdeal.isNoetherian, LieSubmodule.instIsNoetherianSubtypeMem, isNoetherian_sup, set_has_maximal_iff_noetherian, isNoetherian_of_submodule_of_noetherian, isNoetherian_top_iff, IsSemisimpleModule.instIsNoetherianOfFinite, isNoetherian_of_ker_bot, isNoetherian_range, LieSubmodule.Quotient.isNoetherian, isFiniteLength_iff_isNoetherian_isArtinian, isNoetherian_of_linearEquiv, IsSimpleModule.instIsNoetherian, isNoetherian_iff, isNoetherian_of_isNoetherianRing_of_finite, isNoetherian_pi', IsIntegralClosure.isNoetherian
IsNoetherianRing 📖	MathDef	46 math math: GradedRing.GradeZero.isNoetherianRing, IsNoetherianRing.of_prime, PrincipalIdealRing.isNoetherianRing, IsBezout.TFAE, AlgebraicGeometry.isNoetherian_iff_of_finite_affine_openCover, instIsNoetherianRingOfIsArtinianRing, IsNoetherianRing.of_prime_ne_bot, IsLocalization.isNoetherianRing, IsLocalization.instIsNoetherianRingLocalization, IsDedekindDomainInv.isNoetherianRing, Algebra.FiniteType.isNoetherianRing, AdjoinRoot.instIsNoetherianRing, Algebra.EssFiniteType.isNoetherianRing, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, isNoetherianRing_of_surjective, isNoetherianRing_iff_ideal_fg, is_noetherian_subring_closure, isNoetherianRing_range, isNoetherianRing_iff, instIsNoetherianRingSubtypePolynomialMemSubalgebraReesAlgebra, integralClosure.isNoetherianRing, AlgebraicGeometry.isNoetherian_iff_of_finite_iSup_eq_top, AlgebraicGeometry.isLocallyNoetherian_Spec, instIsNoetherianRingMatrix, MvPolynomial.isNoetherianRing_fin, PowerSeries.isNoetherianRing, MvPolynomial.isNoetherianRing_fin_0, isNoetherianRing_rangeS, AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, isDedekindRing_iff, MvPolynomial.isNoetherianRing, Ideal.Quotient.isNoetherianRing, instIsNoetherianRingProd, AlgHom.isNoetherianRing_range, isDedekindDomain_iff, isNoetherianRing_of_fg, IsNoetherianRing.of_finite, AlgebraicGeometry.instIsNoetherianRingCarrierStalkCommRingCatPresheafOfIsLocallyNoetherian, IsSemiprimaryRing.isNoetherianRing_iff_jacobson_fg, isNoetherianRing_of_ringEquiv, Polynomial.isNoetherianRing, IsIntegralClosure.isNoetherianRing, PowerSeries.instIsNoetherianRing, AlgebraicGeometry.isNoetherian_Spec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNoetherianRing_iff 📖	mathematical	—	IsNoetherianRing IsNoetherian NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	—
isNoetherianRing_iff_ideal_fg 📖	mathematical	—	IsNoetherianRing Ideal.FG	—	isNoetherianRing_iff isNoetherian_def
isNoetherian_def 📖	mathematical	—	IsNoetherian Submodule.FG	—	IsNoetherian.noetherian
isNoetherian_iff 📖	mathematical	—	IsNoetherian Submodule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder	—	isNoetherian_iff' isWellFounded_iff
isNoetherian_iff' 📖	mathematical	—	IsNoetherian WellFoundedGT Submodule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder	—	Submodule.fg_iff_compact List.TFAE.out CompleteLattice.wellFoundedGT_characterisations
isNoetherian_iff_fg_wellFounded 📖	mathematical	—	IsNoetherian WellFoundedGT Submodule Submodule.FG Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder	—	OrderEmbedding.wellFoundedLT instWellFoundedLTOrderDualOfWellFoundedGT wellFoundedGT WellFounded.has_min IsWellFounded.wf Submodule.fg_bot bot_le LE.le.antisymm Set.not_subset eq_of_le_of_not_lt le_sup_right Submodule.FG.sup Finset.coe_singleton sup_le Submodule.span_singleton_le_iff_mem le_sup_left Submodule.mem_span_singleton_self
isNoetherian_mk 📖	mathematical	—	IsNoetherian	—	isNoetherian_iff'
isNoetherian_of_le 📖	mathematical	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	IsNoetherian SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module	—	isNoetherian_submodule le_trans
isNoetherian_submodule 📖	mathematical	—	IsNoetherian Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.FG	—	RingHomSurjective.ids Submodule.range_subtype Submodule.FG.map Submodule.map_comap_eq_self Submodule.fg_of_fg_map_injective Subtype.val_injective Submodule.map_subtype_le
isNoetherian_submodule' 📖	mathematical	—	IsNoetherian Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module	—	isNoetherian_submodule IsNoetherian.noetherian
isNoetherian_submodule_left 📖	mathematical	—	IsNoetherian Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.FG Submodule.instMin	—	isNoetherian_submodule inf_le_left inf_of_le_right
isNoetherian_submodule_right 📖	mathematical	—	IsNoetherian Submodule SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.FG Submodule.instMin	—	isNoetherian_submodule inf_le_right inf_of_le_left
monotone_stabilizes_iff_noetherian 📖	mathematical	—	DFunLike.coe OrderHom Submodule Nat.instPreorder PartialOrder.toPreorder Submodule.instPartialOrder OrderHom.instFunLike IsNoetherian	—	isNoetherian_iff' wellFoundedGT_iff_monotone_chain_condition
set_has_maximal_iff_noetherian 📖	mathematical	—	Submodule Set Set.instMembership Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder IsNoetherian	—	isNoetherian_iff WellFounded.wellFounded_iff_has_min
wellFoundedGT 📖	mathematical	—	WellFoundedGT Submodule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder	—	IsNoetherian.wellFoundedGT

---

← Back to Index