change g (h (ζ : Lˣ)) = _
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 }
⊢ ↑g (↑h ↑↑ζ) = ↑↑(ζ ^ ZMod.val (χ n g * χ n h))