aeval_zeta — Mathlib

English

There is an isomorphism between automorphisms of the cyclotomic extension and units of Z/nZ, given by the action on a primitive root.

Русский

Существует изоморфизм автоморфизмов циклотомического расширения и элементов-единиц Z/nZ, действующий на примитивный корень.

LaTeX

$$$(\mathrm{Aut}_K(L)) \simeq (\mathbb{Z}/n\mathbb{Z})^{\times}$ via f(μ) = μ^k$$

Lean4

theorem aeval_zeta [IsDomain B] [NeZero (n : B)] : aeval (zeta n A B) (cyclotomic n A) = 0 :=
  by
  rw [aeval_def, ← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff]
  exact zeta_spec n A B

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