Commit 2025-05-03 07:23 108f3643

View on Github →

feat(Algebra): finiteness of associated primes (#24242) In this PR we proved the finiteness of associated primes for finitely generated modules over notherian ring. Mainly from https://github.com/acmepjz/lean-iwasawa/blob/master/Iwasawalib/RingTheory/CharacteristicIdeal/Basic.lean authored by @acmepjz

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Range.lean

added theorem Submodule.submoduleOf_self

added theorem Submodule.submoduleOf_sup_of_le

Modified Mathlib/LinearAlgebra/Span/Basic.lean

added theorem LinearMap.range_toSpanSingleton

added theorem LinearMap.submoduleOf_span_singleton_of_mem

Modified Mathlib/Order/BoundedOrder/Lattice.lean

added theorem WellFoundedGT.induction_top

added theorem WellFoundedLT.induction_bot

Created Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean

added theorem IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime

added theorem IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime

added def Submodule.IsQuotientEquivQuotientPrime

added theorem Submodule.isQuotientEquivQuotientPrime_iff

added theorem associatedPrimes.finite

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean

added theorem Ideal.Quotient.span_singleton_one