rw [map_pow, eq_one_mod_one_sub, one_pow]
case intro.intro
p : ℕ+
K : Type ?u.65835
inst✝³ : Field K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
inst✝² : NumberField K
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsDomain A
ζ : A
hζ : IsPrimitiveRoot ζ ↑p
k : ℕ
hμ : (ζ ^ k) ^ ↑p = 1
⊢ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) (ζ ^ k) = 1
no goals