@[reducible, inline]

noncomputable abbrev idealNorm {O : Type u_1} [CommRing O] [Nontrivial O] [IsDedekindDomain O] [Module.Free ℤ O] : Ideal O →*₀ ℕ

theorem idealNorm_span_singleton_numberField {K : Type u_1} [Field K] [NumberField K] (α : NumberField.RingOfIntegers K) : idealNorm (Ideal.span {α}) = ((Algebra.norm ℤ) α).natAbs