integer_power_of_ringEquiv' — Mathlib

English

If g is a ring automorphism of L, there exists an integer m such that g(t) = t^m for every nth root t of unity in L.

Русский

Если g — автоморфизм кольца L, существует целое число m такое, что для каждого t-ного корня единства t в L выполняется g(t) = t^m.

LaTeX

$$$\\exists m\\in \\mathbb{Z}\\; \\forall t\\in \\text{rootsOfUnity}(n,L),\\; g(t)=t^{m}$$$

Lean4

theorem integer_power_of_ringEquiv' (g : L ≃+* L) : ∃ m : ℤ, ∀ t ∈ rootsOfUnity n L, g (t : Lˣ) = (t ^ m : Lˣ) := by
  simpa using rootsOfUnity.integer_power_of_ringEquiv n g

Похожие утверждения