rw [← map_dvd_iff (equiv p), map_intCast]
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))
p : ℕ
hpri : Fact p.Prime
n : CyclotomicIntegers p
hn : n ≠ 0
⊢ (equiv p) n ∣ ↑((Algebra.norm ℤ) ((equiv p) n))