aux — Mathlib

English

A variant of the previous fact for RingEquiv rather than a Ring automorphism, asserting the same exponent-on-roots phenomenon.

Русский

Вариант предыдущего факта для RingEquiv, утверждающий ту же экспонентную зависимость на корнях единства.

LaTeX

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

Lean4

/-- `modularCyclotomicCharacter_aux g n` is a non-canonical auxiliary integer `j`,
  only well-defined modulo the number of `n`-th roots of unity in `L`, such that `g(ζ)=ζ^j`
  for all `n`-th roots of unity `ζ` in `L`. -/
noncomputable def aux (g : L ≃+* L) (n : ℕ) [NeZero n] : ℤ :=
  (rootsOfUnity.integer_power_of_ringEquiv n g).choose

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