exact one_mem _
case inl
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
R : Type u_2
S : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra R S
inst✝ : IsCyclotomicExtension {2} R S
x : S
this : x ∈ Algebra.adjoin R {b | b = 1 ∨ b = -1}
⊢ 1 ∈ ↑⊥
no goals