pow — Mathlib

English

For any integer z, mapFun f sends the Witt vector corresponding to z to z in the target Witt vectors: mapFun f (z : 𝕎 R) = z.

Русский

Для любого целого z отображение mapFun f отправляет Witt-вектор, соответствующий z, в такой же Witt-вектор в 𝕎 S: mapFun f (z : 𝕎 R) = z.

LaTeX

$$$\\mathrm{WittVector.mapFun}\\, f\\, (z : \\mathbb{W}R) = z$$$

Lean4

theorem pow (n : ℕ) : mapFun f (x ^ n) = mapFun f x ^ n := by map_fun_tac

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