ghostComponent_teichmuller — Mathlib

English

The nth ghost component of teichmuller p r is r^(p^n).

Русский

N-ая призрачная компонента Teichmüller-поднятия равна r^(p^n).

LaTeX

$$$\\mathrm{ghostComponent}\, n\\; (\\mathrm{teichmuller}\\ p\\; r) = r^{p^n}$$$

Lean4

/-- The `n`-th ghost component of `teichmuller p r` is `r ^ p ^ n`. -/
@[simp]
theorem ghostComponent_teichmuller (r : R) (n : ℕ) : ghostComponent n (teichmuller p r) = r ^ p ^ n :=
  ghostComponent_teichmullerFun _ _ _

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