∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsFractionRing 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] [inst_6 : IsDedekindDomain 𝒪] [inst_7 : CharZero 𝒪]
  [Module.Finite ℤ 𝒪], ↑(NumberField.discr K) ∈ differentIdeal ℤ 𝒪