obtain ⟨k, -, rfl⟩ := hζ.eq_pow_of_pow_eq_one hμ p.pos
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
μ : A
hμ : μ ^ ↑p = 1
⊢ (algebraMap A (A ⧸ Ideal.span {ζ - 1})) μ = 1
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