apply Subsingleton.elim
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
this✝ : 1 ≤ Fintype.card { x // x ∈ rootsOfUnity n L }
h : 1 = Fintype.card { x // x ∈ rootsOfUnity n L }
this : Subsingleton { x // x ∈ rootsOfUnity n L }
⊢ ζ = 1
no goals