toFun_spec'' — Mathlib

English

Let L be a domain with a commutative ring structure. For every field automorphism g of L and every n > 0, if t is a primitive n-th root of unity in L, then g(t) = t^{χ₀(n,g).val}, where χ₀ is the mod-n cyclotomic character.

Русский

Пусть L — область с коммутативной структурой кольца. Для любого автоморфизма g поля L и любого натурального n>0, если t — примитивный корень из единицы степени n в L, то выполняется g(t) = t^{χ₀(n,g).val}, где χ₀ — модульная циклотомическая характеристика.

LaTeX

$$$ g(t) = t^{\\big(\\chi_{0}(n,g)\\big).val} $$$

Lean4

theorem toFun_spec'' (g : L ≃+* L) {n : ℕ} [NeZero n] {t : L} (ht : IsPrimitiveRoot t n) : g t = t ^ (χ₀ n g).val :=
  toFun_spec' g (SetLike.coe_mem ht.toRootsOfUnity)

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