ext1
case h.e'_4
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑((Algebra.norm ℤ) ((equiv p) n)) =
    (algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n))
case h.e'_4.h
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ ↑↑((Algebra.norm ℤ) ((equiv p) n)) =
    ↑((algebraMap (𝓞 ℚ) (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ((RingOfIntegers.norm ℚ) ((equiv p) n)))