exact ⟨m, by simp [← hm]⟩
case intro
L : Type u
inst✝ : Field L
n : ℕ+
g : L ≃+* L
m : ℤ
hm : ∀ (g_1 : { x // x ∈ rootsOfUnity n L }), ↑(MulEquiv.toMonoidHom (RingEquiv.restrictRootsOfUnity g n)) g_1 = g_1 ^ m
⊢ ∃ m, ∀ (t : { x // x ∈ rootsOfUnity n L }), ↑g ↑↑t = ↑↑(t ^ m)
no goals