teichmullerFun — Mathlib

English

The underlying function of teichmullerFun p r is a Witt vector whose n-th component is r if n=0 and 0 otherwise.

Русский

При фиксированном p и r функция teichmullerFun p r задаёт Witt-вектор, у которого n-й компонент равна r, если n=0, и равна 0 в противном случае.

LaTeX

$$$(\\mathrm{teichmullerFun}\\ p \\ r)(n) = \\begin{cases} r & n = 0 \\\\ 0 & n > 0 \\end{cases}$$$

Lean4

/-- The underlying function of the monoid hom `WittVector.teichmuller`.
The `0`-th coefficient of `teichmullerFun p r` is `r`, and all others are `0`.
-/
def teichmullerFun (r : R) : 𝕎 R :=
  ⟨fun n => if n = 0 then r else 0⟩

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