Commit 2025-11-19 16:14 0856a895

View on Github →

feat: power series over a noetherian ring is noetherian (#31149) We add that the power series ring over a noetherian ring is noetherian.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/SpanRank.lean

added theorem Ideal.spanFinrank_map_le_of_fg

added theorem Ideal.spanRank_map_le

added theorem Submodule.spanFinrank_map_le_of_fg

added theorem Submodule.spanFinrank_of_not_fg

added theorem Submodule.spanRank_map_le

Created Mathlib/RingTheory/PowerSeries/Ideal.lean

added theorem PowerSeries.eq_of_le_of_X_notMem_of_fg_of_isPrime

added theorem PowerSeries.eq_span_insert_X_of_X_mem_of_span_eq

added theorem PowerSeries.exist_eq_span_eq_ncard_of_X_notMem

added theorem PowerSeries.fg_iff_of_isPrime

added theorem PowerSeries.map_constantCoeff_le_self_of_X_mem

added theorem PowerSeries.spanFinrank_eq_spanFinrank_map_constantCoeff_of_X_notMem_of_fg_of_isPrime

added theorem PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem

added theorem PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_isPrime

Modified Mathlib/RingTheory/PowerSeries/Trunc.lean

added theorem PowerSeries.monomial_eq_C_mul_X_pow

modified def PowerSeries.trunc

added theorem PowerSeries.trunc_X_pow_self_mul

deleted theorem PowerSeries.trunc_add

added theorem PowerSeries.trunc_apply

added theorem PowerSeries.trunc_sub

deleted theorem PowerSeries.trunc_zero

Modified docs/references.bib