intro ζ
L : Type u
inst✝ : Field L
n : ℕ+
⊢ ∀ (t : { x // x ∈ rootsOfUnity n L }), t ^ ZMod.val (χ n (RingEquiv.refl L)) = t ^ ZMod.val 1
L : Type u
inst✝ : Field L
n : ℕ+
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n (RingEquiv.refl L)) = ζ ^ ZMod.val 1