The full norm polynomial is the minimal polynomial raised to the index of the subfield generated by its parameter. This retains the multiplicity that distinguishes ordinary and exceptional norm curves.

theorem CCDN.integerNormPolynomial_map_eq_minpoly_pow_algebraicClosure (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) : Polynomial.map (Int.castRingHom (AlgebraicClosure ℚ)) (integerNormPolynomial K β) = Polynomial.map (algebraMap ℚ (AlgebraicClosure ℚ)) (minpoly ℚ ↑β) ^ Module.finrank (↥ℚ⟮↑β⟯) K

Over an algebraic closure of ℚ, the integer norm polynomial of β is the minimal polynomial of β over ℚ raised to the power [K : ℚ(β)].