Separation by powers of all maximal ideals

For a finite module over a noetherian commutative ring, the intersection of all positive powers of all maximal ideals acting on the module is zero. The quantifier over all maximal ideals is essential: the powers of one maximal ideal need not separate a nonlocal ring.

The proof uses Mathlib's Krull intersection criterion Ideal.mem_iInf_smul_pow_eq_bot_iff at a maximal ideal containing the annihilator of an element.

theorem Ideal.iInf_isMaximal_pow_smul_eq_bot {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : ⨅ (m : Ideal R), ⨅ (_ : m.IsMaximal), ⨅ (n : ℕ), ⨅ (_ : 0 < n), m ^ n • ⊤ = ⊥

Positive powers of all maximal ideals separate a finite module over a noetherian ring.

theorem Ideal.iInf_isMaximal_pow_eq_bot {R : Type u_1} [CommRing R] [IsNoetherianRing R] : ⨅ (m : Ideal R), ⨅ (_ : m.IsMaximal), ⨅ (n : ℕ), ⨅ (_ : 0 < n), m ^ n = ⊥

Positive powers of all maximal ideals of a noetherian ring have zero intersection.