zsmul — Mathlib

English

For any natural n, mapFun f sends the Witt vector corresponding to n to the same n in the target Witt vectors: mapFun f (n : 𝕎 R) = (n : 𝕎 S).

Русский

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

LaTeX

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

Lean4

theorem zsmul (z : ℤ) (x : WittVector p R) : mapFun f (z • x) = z • mapFun f x := by map_fun_tac

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