rw [ModularCyclotomicCharacter_aux_spec g n t, ← zpow_ofNat, ModularCyclotomicCharacter.toFun,
    ZMod.val_int_cast, ←Group.pow_eq_zpow_mod _ pow_card_eq_one]
L : Type u
inst✝ : Field L
n✝ : ℕ+
g : L ≃+* L
n : ℕ+
t : { x // x ∈ rootsOfUnity n L }
⊢ ↑g ↑↑t = ↑↑(t ^ ZMod.val (χ n g))
no goals