spec — Mathlib

English

The unique exponent c satisfying ∀ t ∈ rootsOfUnity n L, g t = t^c is precisely χ₀(n,g) when transported through the natural isomorphism.

Русский

Уникальный показатель c, удовлетворяющий ∀ t ∈ rootsOfUnity n L, g t = t^c, равен χ₀(n,g) через естественный изоморфизм.

LaTeX

$$$\\forall t∈\\mathrm{rootsOfUnity}_n L\\, (g t = t^c) \\iff c=χ_{0}(n,g)$$$

Lean4

theorem spec (p : ℕ) [Fact p.Prime] {n : ℕ} [∀ i, HasEnoughRootsOfUnity L (p ^ i)] (g : L ≃+* L) (t : L)
    (ht : t ^ p ^ n = 1) : g t = t ^ ((cyclotomicCharacter L p g).val.toZModPow n).val :=
  toFun_spec p g (rootsOfUnity.mkOfPowEq _ ht)

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