exact Ideal.mul_mem_left _ _ (pow_sub_intGalConj_mem hp α)
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
this✝ : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
this : Fact (↑p).Prime
k : ℕ
H : u * ((unitGalConj K p) u)⁻¹ = (hζ.unit' ^ k) ^ 2
⊢ ↑u * (α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)) ∈ Ideal.span {↑↑p}
no goals