Commit 2024-11-11 10:06 2567852e

chore(RingTheory/Noetherian): split Noetherian.lean (#18734) This PR splits RingTheory/Noetherian.lean into the following files:

• Noetherian/Defs.lean: definition of IsNoetherian and IsNoetherianRing; proof of isNoetherian_iff
• Noetherian/Filter.lean: ascending chain condition, expressed in terms of filters
• Noetherian/Orzech.lean: Orzech's theorem and property
• Noetherian/Nilpotent.lean: nilpotent ideals in Noetherian rings
• Noetherian/UniqueFactorization.lean: Noetherian implies unique factorization This change should also clean up the import graph for LinearAlgebra somewhat, especially in combination with PR #18731. Note that there was a timeout in Topology/Sheaves/Stalks.lean caused by the instance search order changing. We can either do a local priority change, or simply avoid importing the slow instances. See also Zulip thread.