Hausdorff-ness for Noetherian rings

theorem IsHausdorff.of_le_jacobson {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] (h : I ≤ ⊥.jacobson) : IsHausdorff I M

theorem IsHausdorff.of_isLocalRing {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] [IsLocalRing R] (h : I ≠ ⊤) : IsHausdorff I M

instance instIsHausdorffMaximalIdeal {R : Type u_1} [CommRing R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] [IsLocalRing R] : IsHausdorff (IsLocalRing.maximalIdeal R) M

theorem IsHausdorff.of_isTorsionFree {R : Type u_1} [CommRing R] (I : Ideal R) (M : Type u_2) [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M] (h : I ≠ ⊤) : IsHausdorff I M

theorem IsHausdorff.of_isDomain {R : Type u_1} [CommRing R] (I : Ideal R) [IsNoetherianRing R] [IsDomain R] (h : I ≠ ⊤) : IsHausdorff I R