Commit 2023-08-16 16:40 d8130a5e

View on Github →

chore: restate isNoetherian_of_fg_of_noetherian' using Module.Finite (and rename). (#6609)

Estimated changes

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/NumberTheory/Cyclotomic/Basic.lean

Modified Mathlib/RingTheory/Adjoin/Tower.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/Filtration.lean

modified theorem Ideal.Filtration.Stable.of_le

modified theorem Ideal.mem_iInf_smul_pow_eq_bot_iff

Modified Mathlib/RingTheory/Noetherian.lean

deleted theorem isNoetherian_of_fg_of_noetherian'

added theorem isNoetherian_of_isNoetherianRing_of_finite