feat(NumberTheory/NumberField/Discriminant): add not_dvd_discr_iff_isUnramifiedIn

A prime `p` does not divide `discr K` if and only if `p` is unramified in the ring of
integers, phrased using the `Algebra.IsUnramifiedIn` predicate.

Author: xroblot

Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

@@ -193,6 +193,20 @@ lemma not_dvd_discr_iff_forall_liesOver [IsIntegralClosure 𝒪 ℤ K] {p : ℤ}
       ← Int.natAbs_pow, Int.natAbs_dvd_natAbs] at this
     exact (dvd_pow_self _ (Ideal.inertiaDeg_pos' ..).ne').trans this
 
+/-- A prime `p` does not divide `discr K` if and only if `p` (as the ideal `span {p}`) is
+unramified in the ring of integers `𝒪`.
+
+Also see `not_dvd_discr_iff_forall_liesOver` and `not_dvd_discr_iff_forall_mem` for variants
+whose RHS does not use `Algebra.IsUnramifiedIn`. -/
+lemma not_dvd_discr_iff_isUnramifiedIn [IsIntegralClosure 𝒪 ℤ K] {p : ℤ} (hp : Prime p) :
+    ¬ p ∣ discr K ↔ Algebra.IsUnramifiedIn 𝒪 (Ideal.span {p}) := by
+  have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
+  have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
+  have := CharZero.of_module (R := 𝒪) K
+  rw [not_dvd_discr_iff_forall_liesOver K 𝒪 hp]
+  exact (Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain'
+    (Ideal.span_singleton_eq_bot.not.mpr hp.ne_zero)).symm
+
 /-- Also see `not_dvd_discr_iff_forall_liesOver` for a slightly easier to prove RHS. -/
 lemma not_dvd_discr_iff_forall_mem [IsIntegralClosure 𝒪 ℤ K] {p : ℤ} (hp : Prime p) :
     ¬ p ∣ discr K ↔ ∀ (P : Ideal 𝒪) (_ : P.IsPrime), ↑p ∈ P →