toFun_spec' — Mathlib

English

Variant of toFun_spec with t as a unit root; expresses the same relation in terms of RingEquiv on units.

Русский

Вариант toFun_spec для единицной группы; выражает ту же зависимость в терминах RingEquiv на единицах.

LaTeX

$$$\\forall t\\in (rootsOfUnity(n,L))\\; g(t) = t^{(toFun(n,g)).val}$$$

Lean4

theorem toFun_spec' (g : L ≃+* L) {n : ℕ} [NeZero n] {t : Lˣ} (ht : t ∈ rootsOfUnity n L) : g t = t ^ (χ₀ n g).val :=
  toFun_spec g ⟨t, ht⟩

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