map_verschiebung — Mathlib

English

The VerschiebungFun is a polynomial map in Witt polynomials; it is encoded via IsPoly for verschiebungFun.

Русский

VerschiebungFun — полиномиальное отображение по координатам Witt; формализуется через IsPoly.

LaTeX

$$$$ \\text{verschiebungFun isPoly} \\,(p, \\text{Witt}) $$$$

Lean4

/-- verschiebung is a natural transformation -/
@[simp]
theorem map_verschiebung (f : R →+* S) (x : 𝕎 R) : map f (verschiebung x) = verschiebung (map f x) :=
  by
  ext ⟨-, -⟩
  · exact f.map_zero
  · rfl

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