(Absolute) Discriminant and Different Ideal

Main results

• NumberField.absNorm_differentIdeal: The norm of differentIdeal ℤ 𝒪 is the absolute discriminant.

theorem NumberField.absNorm_differentIdeal {K : Type u_1} {𝒪 : Type u_2} [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsFractionRing 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] [IsDedekindDomain 𝒪] [CharZero 𝒪] [Module.Finite ℤ 𝒪] : Ideal.absNorm (differentIdeal ℤ 𝒪) = (discr K).natAbs

theorem NumberField.discr_mem_differentIdeal {K : Type u_1} {𝒪 : Type u_2} [Field K] [NumberField K] [CommRing 𝒪] [Algebra 𝒪 K] [IsFractionRing 𝒪 K] [IsIntegralClosure 𝒪 ℤ K] [IsDedekindDomain 𝒪] [CharZero 𝒪] [Module.Finite ℤ 𝒪] : ↑(discr K) ∈ differentIdeal ℤ 𝒪