simp only [pow_eq_pow_iff_modEq, ← ZMod.nat_cast_eq_nat_cast_iff, SubmonoidClass.coe_pow,
  ZMod.nat_cast_val, Nat.cast_mul, ZMod.cast_mul (m := orderOf ζ) orderOf_dvd_card_univ]
case a.a.e_self.e_self
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ζ ^ ZMod.val (χ n h * χ n g) = ζ ^ (ZMod.val (χ n h) * ZMod.val (χ n g))
no goals