rw [spec, spec, mul_comm, ← pow_mul, eq_comm]
case a.a
L : Type u
inst✝ : Field L
n : ℕ+
g h : L ≃+* L
ζ : { x // x ∈ rootsOfUnity n L }
⊢ ↑g (↑h ↑↑ζ) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))
case a.a
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)))