Commit 2026-04-11 09:00 35e1c7ee

View on Github →

feat(RingTheory/Flat/FaithfullyFlat/Basic): prove IsNoetherian and IsArtinian from faithfully flat base change (#37104) This PR proves that if the base change of a module M along a faithfully flat ring homomorphism is Noetherian or Artinian, then so is M. The file Artinian/Module has become rather heavy, so I split off a Artinian/Defs file to avoid the large import.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem Submodule.baseChange_mono

Created Mathlib/RingTheory/Artinian/Defs.lean

added theorem IsArtinian.induction

added theorem isArtinianRing_iff

added theorem isArtinian_iff

Modified Mathlib/RingTheory/Artinian/Module.lean

deleted theorem IsArtinian.induction

deleted theorem isArtinianRing_iff

deleted theorem isArtinian_iff

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

added theorem Submodule.IsArtinian.of_isArtinian_tensorProduct_of_faithfullyFlat

added theorem Submodule.IsNoetherian.of_isNoetherian_tensorProduct_of_faithfullyFlat

added def Submodule.baseChangeOrderEmbedding

added theorem Submodule.baseChange_inj

added theorem Submodule.baseChange_injective

added theorem Submodule.baseChange_le_iff