Basic

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

Statistics

Metric	Count
Definitions	0
Theorems `disjoint_partialSups_eventually_bot`, `induction`, `subsingleton_of_injective`, `of_finite`, `isNoetherian_iff`, `finite_of_isNoetherian`, `set_finite_of_isNoetherian`, `isNoetherian_iff_of_bijective`, `of_injective`, `finite`, `exists_finite_presentation`, `instFiniteSubtypeMemIdealOfIsNoetherian`, `of_le`, `of_le_of_isNoetherian`, `finite_ne_bot_of_iSupIndep`, `fg_of_injective`, `fg_of_ker_bot`, `instIsNoetherianRingForallOfFinite`, `instIsNoetherianRingProd`, `isNoetherianRing_of_ringEquiv`, `isNoetherianRing_of_surjective`, `isNoetherianRing_range`, `isNoetherianRing_rangeS`, `isNoetherian_iSup`, `isNoetherian_iff_submodule_quotient`, `isNoetherian_linearMap`, `isNoetherian_linearMap_pi`, `isNoetherian_of_fg_of_noetherian`, `isNoetherian_of_finite`, `isNoetherian_of_injective`, `isNoetherian_of_isNoetherianRing_of_finite`, `isNoetherian_of_ker_bot`, `isNoetherian_of_linearEquiv`, `isNoetherian_of_range_eq_ker`, `isNoetherian_of_submodule_of_noetherian`, `isNoetherian_of_subsingleton`, `isNoetherian_of_surjective`, `isNoetherian_of_tower`, `isNoetherian_pi`, `isNoetherian_pi'`, `isNoetherian_prod`, `isNoetherian_quotient`, `isNoetherian_range`, `isNoetherian_span_of_finite`, `isNoetherian_sup`, `isNoetherian_top_iff`	46
Total	46

IsNoetherian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`disjoint_partialSups_eventually_bot` 📖	mathematical	`Disjoint` `Submodule` `Submodule.instPartialOrder` `Submodule.instOrderBot` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `OrderHom.instFunLike` `partialSups` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder`	`Bot.bot` `Submodule.instBot`	—	`monotone_stabilizes_iff_noetherian` `Disjoint.eq_bot_of_ge` `sup_eq_left` `partialSups_add_one` `le_add_right` `Nat.instCanonicallyOrderedAdd`
`induction` 📖	—	—	—	—	`IsWellFounded.induction` `wellFoundedGT`
`subsingleton_of_injective` 📖	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike`	—	—	`by_contra` `LinearMap.exists_finsupp_nat_of_prod_injective` `Infinite.not_finite` `instInfiniteNat` `WellFoundedGT.finite_of_iSupIndep` `wellFoundedGT` `RingHomSurjective.ids` `LinearMap.iSupIndep_map` `iSupIndep_range_lsingle` `Submodule.ne_bot_iff`

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_finite` 📖	mathematical	—	`IsNoetherianRing` `Ring.toSemiring`	—	`isNoetherian_of_tower` `isNoetherian_of_isNoetherianRing_of_finite`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNoetherian_iff` 📖	mathematical	—	`IsNoetherian`	—	`RingHomInvPair.ids` `isNoetherian_of_linearEquiv`

LinearIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_of_isNoetherian` 📖	mathematical	`LinearIndependent`	`Finite`	—	`WellFoundedGT.finite_of_iSupIndep` `wellFoundedGT` `iSupIndep_span_singleton` `ne_zero`
`set_finite_of_isNoetherian` 📖	mathematical	`LinearIndependent` `Set` `Set.instMembership`	`Set.Finite`	—	`finite_of_isNoetherian`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNoetherian_iff_of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `instFunLike`	`IsNoetherian`	—	`StrictMono.wellFoundedGT` `OrderIso.strictMono`

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_finite_presentation` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike`	—	`Finite.exists_fin'` `RingHomCompTriple.ids` `RingHomInvPair.ids` `Finite.of_fintype` `Free.finsupp` `Free.Module.free_shrink` `Free.self` `Finite.finsupp` `Finite.Module.finite_shrink` `Finite.self`
`instFiniteSubtypeMemIdealOfIsNoetherian` 📖	mathematical	—	`Finite` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CommSemiring.toSemiring` `Submodule.addCommMonoid` `Submodule.module'` `Algebra.toSMul` `Algebra.toModule` `IsScalarTower.right`	—	`IsNoetherian.finite` `IsScalarTower.right` `isNoetherian_submodule'`

Module.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Module.Finite`	—	`fg_of_injective`

Module.IsNoetherian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Module.Finite`	—	`IsNoetherian.noetherian`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_ne_bot_of_iSupIndep` 📖	mathematical	`iSupIndep` `Submodule` `completeLattice`	`Set.Finite` `setOf` `Bot.bot` `instBot`	—	`WellFoundedGT.finite_ne_bot_of_iSupIndep` `wellFoundedGT`

Submodule.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_le` 📖	—	`Submodule.FG` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	—	`of_le_of_isNoetherian` `isNoetherian_of_isNoetherianRing_of_finite` `Module.Finite.iff_fg`
`of_le_of_isNoetherian` 📖	mathematical	`Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`Submodule.FG`	—	`isNoetherian_submodule`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fg_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Submodule.FG`	—	`IsNoetherian.noetherian` `isNoetherian_of_injective`
`fg_of_ker_bot` 📖	mathematical	`LinearMap.ker` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `Submodule.instBot`	`Submodule.FG`	—	`IsNoetherian.noetherian` `isNoetherian_of_ker_bot`
`instIsNoetherianRingForallOfFinite` 📖	mathematical	`IsNoetherianRing`	`Pi.semiring`	—	`Finite.induction_empty_option` `isNoetherianRing_of_ringEquiv` `isNoetherian_of_subsingleton` `Unique.instSubsingleton` `PEmpty.instIsEmpty` `instIsNoetherianRingProd`
`instIsNoetherianRingProd` 📖	mathematical	—	`IsNoetherianRing` `Prod.instSemiring`	—	`IsNoetherianRing.eq_1` `isNoetherian_iff'` `OrderEmbedding.wellFoundedGT` `Prod.wellFoundedGT`
`isNoetherianRing_of_ringEquiv` 📖	mathematical	—	`IsNoetherianRing`	—	`isNoetherianRing_of_surjective` `Equiv.surjective`
`isNoetherianRing_of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`IsNoetherianRing`	—	`OrderEmbedding.wellFounded` `RingHom.instRingHomClass` `IsNoetherian.wf`
`isNoetherianRing_range` 📖	mathematical	—	`IsNoetherianRing` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `Ring.toSemiring` `Subring.toRing`	—	`isNoetherianRing_rangeS`
`isNoetherianRing_rangeS` 📖	mathematical	—	`IsNoetherianRing` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `RingHom.rangeS` `Subsemiring.toSemiring`	—	`isNoetherianRing_of_surjective` `RingHom.rangeSRestrict_surjective`
`isNoetherian_iSup` 📖	mathematical	`IsNoetherian` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`Finite.induction_empty_option` `Equiv.iSup_comp` `iSup_of_empty` `PEmpty.instIsEmpty` `isNoetherian_of_finite` `Finite.of_fintype` `iSup_option` `isNoetherian_sup`
`isNoetherian_iff_submodule_quotient` 📖	mathematical	—	`IsNoetherian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`isNoetherian_submodule'` `isNoetherian_quotient` `isNoetherian_of_range_eq_ker` `RingHomSurjective.ids` `Submodule.ker_mkQ` `Submodule.range_subtype`
`isNoetherian_linearMap` 📖	mathematical	—	`IsNoetherian` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`smulCommClass_self` `Module.Finite.exists_fin'` `SMulCommClass.symm` `LinearMap.instSMulCommClass` `RingHomCompTriple.ids` `isNoetherian_of_injective` `isNoetherian_linearMap_pi` `Finite.of_fintype` `Function.Surjective.injective_linearMapComp_right`
`isNoetherian_linearMap_pi` 📖	mathematical	—	`IsNoetherian` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddCommGroup.toAddCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing`	—	`isNoetherian_of_linearEquiv` `smulCommClass_self` `isNoetherian_pi'`
`isNoetherian_of_fg_of_noetherian` 📖	mathematical	`Submodule.FG` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`IsNoetherian` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`isNoetherian_of_isNoetherianRing_of_finite` `Module.Finite.of_fg`
`isNoetherian_of_finite` 📖	mathematical	—	`IsNoetherian`	—	`Set.toFinite` `Subtype.finite` `Set.Finite.coe_toFinset` `Submodule.span_eq`
`isNoetherian_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`IsNoetherian`	—	`isNoetherian_of_linearEquiv` `RingHomSurjective.invPair` `RingHomInvPair.ids` `isNoetherian_submodule'`
`isNoetherian_of_isNoetherianRing_of_finite` 📖	mathematical	—	`IsNoetherian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Module.Finite.exists_fin'` `isNoetherian_of_surjective` `RingHomSurjective.ids` `LinearMap.range_eq_top` `isNoetherian_pi'` `Finite.of_fintype`
`isNoetherian_of_ker_bot` 📖	mathematical	`LinearMap.ker` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `Bot.bot` `Submodule` `Submodule.instBot`	`IsNoetherian`	—	`isNoetherian_of_linearEquiv` `RingHomSurjective.invPair` `RingHomInvPair.ids` `LinearMap.ker_eq_bot` `isNoetherian_submodule'`
`isNoetherian_of_linearEquiv` 📖	mathematical	—	`IsNoetherian`	—	`RingHomInvPair.ids` `isNoetherian_of_surjective` `LinearEquiv.range`
`isNoetherian_of_range_eq_ker` 📖	mathematical	`LinearMap.range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.ker`	`IsNoetherian`	—	`RingHomSurjective.ids` `wellFounded_gt_exact_sequence` `Submodule.instIsModularLattice` `wellFoundedGT` `isNoetherian_quotient` `isNoetherian_submodule'` `le_rfl` `LinearMap.ker_eq_bot` `Submodule.ker_liftQ_eq_bot` `LinearMap.surjective_rangeRestrict` `Submodule.map_comap_eq` `Submodule.range_liftQ` `inf_comm` `Submodule.comap_map_eq` `LinearMap.ker_rangeRestrict`
`isNoetherian_of_submodule_of_noetherian` 📖	mathematical	—	`IsNoetherian` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`OrderEmbedding.wellFounded` `IsNoetherian.wf`
`isNoetherian_of_subsingleton` 📖	mathematical	—	`IsNoetherian`	—	`isNoetherian_of_finite` `Finite.of_subsingleton` `Module.subsingleton`
`isNoetherian_of_surjective` 📖	mathematical	`LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Top.top` `Submodule` `Submodule.instTop`	`IsNoetherian`	—	`RingHomSurjective.ids` `Submodule.map_comap_eq_self` `le_top` `Submodule.FG.map` `IsNoetherian.noetherian`
`isNoetherian_of_tower` 📖	mathematical	—	`IsNoetherian`	—	`OrderEmbedding.wellFounded` `IsNoetherian.wf`
`isNoetherian_pi` 📖	mathematical	`IsNoetherian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`Pi.addCommMonoid` `Pi.module`	—	`Finite.induction_empty_option` `isNoetherian_of_linearEquiv` `isNoetherian_of_finite` `Finite.of_fintype` `PEmpty.instIsEmpty` `RingHomInvPair.ids` `isNoetherian_prod`
`isNoetherian_pi'` 📖	mathematical	—	`IsNoetherian` `Ring.toSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.Function.module`	—	`isNoetherian_pi`
`isNoetherian_prod` 📖	mathematical	—	`IsNoetherian` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule`	—	`Submodule.fg_of_fg_map_of_fg_inf_ker` `IsNoetherian.noetherian` `RingHomSurjective.ids` `LinearMap.mem_ker` `Submodule.FG.map` `Submodule.map_comap_eq_self`
`isNoetherian_quotient` 📖	mathematical	—	`IsNoetherian` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module'`	—	`isNoetherian_of_surjective` `LinearMap.IsScalarTower.compatibleSMul` `Submodule.Quotient.isScalarTower` `RingHomSurjective.ids` `LinearMap.range_eq_top` `Submodule.mkQ_surjective`
`isNoetherian_range` 📖	mathematical	—	`IsNoetherian` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`isNoetherian_of_surjective` `RingHomSurjective.ids` `LinearMap.range_rangeRestrict`
`isNoetherian_span_of_finite` 📖	mathematical	—	`IsNoetherian` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Submodule.addCommMonoid` `Submodule.module`	—	`isNoetherian_of_fg_of_noetherian` `Submodule.fg_def`
`isNoetherian_sup` 📖	mathematical	—	`IsNoetherian` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `isNoetherian_range` `isNoetherian_prod` `Submodule.range_subtype` `LinearMap.range_coprod`
`isNoetherian_top_iff` 📖	mathematical	—	`IsNoetherian` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Top.top` `Submodule.instTop` `Submodule.addCommMonoid` `Submodule.module`	—	`LinearEquiv.isNoetherian_iff`

---

← Back to Index