aux_spec — Mathlib

English

For any automorphism g of L, the value of g on nth roots of unity is determined by the auxiliary cyclotomic character: g(t) = t^{aux g n} for t in rootsOfUnity.

Русский

Для любого автоморфизма g кольца L значение на n-й корень единства задаётся дополнительной циклотомической характеристикой: g(t)=t^{aux g n} для t из rootsOfUnity.

LaTeX

$$$\\forall t\\in \\text{rootsOfUnity}(n,L),\\; g(t)=t^{\\operatorname{aux}g\,n}$$$

Lean4

theorem aux_spec (g : L ≃+* L) (n : ℕ) [NeZero n] :
    ∀ t : rootsOfUnity n L, g (t : Lˣ) = (t ^ (modularCyclotomicCharacter.aux g n) : Lˣ) :=
  (rootsOfUnity.integer_power_of_ringEquiv n g).choose_spec

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