Minimal primes over a colon ideal

We prove that a minimal prime over an ideal of the form N.colon {x} in a Noetherian ring is itself an ideal of the form N.colon {x'}.

theorem Submodule.exists_eq_colon_of_mem_minimalPrimes {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {I : Ideal R} {x : M} [IsNoetherianRing R] (hI : I ∈ (N.colon {x}).minimalPrimes) : ∃ (x' : M), I = N.colon {x'}

A minimal prime over an ideal of the form N.colon {x} in a Noetherian ring is itself an ideal of the form N.colon {x'}.