verschiebungFun_isPoly — Mathlib

English

The VerschiebungFun function is a polynomial map in Witt coordinates; there exists a polynomial describing verschiebungFun.

Русский

Функция verschiebungFun является полиномиальным отображением по координатам Witt.

LaTeX

$$$$ \\text{IsPoly}(p, \\text{verschiebungFun}). $$$$

Lean4

/-- `WittVector.verschiebung` has polynomial structure given by `WittVector.verschiebungPoly`.
-/
instance verschiebungFun_isPoly : IsPoly p fun R _Rcr => @verschiebungFun p R _Rcr :=
  by
  use verschiebungPoly
  simp only [aeval_verschiebung_poly', forall₃_true_iff]
    -- We add this example as a verification that Lean 4's instance resolution can handle the `IsPoly`
    -- typeclass, whereas Lean 3 needed a bespoke `@[is_poly]` attribute.

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