∀ {p : ℕ} {K : Type u} (L : Type v) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Fact (Nat.Prime p)] [inst_4 : IsCyclotomicExtension {p} K L],
  Irreducible (Polynomial.cyclotomic p K) → p ≠ 2 → (Algebra.norm K) (IsCyclotomicExtension.zeta p K L - 1) = ↑p