zeroIsPoly — Mathlib

English

The polynomial obtained by binding the zero polynomial with the Witt polynomial is identically zero.

Русский

Полином, полученный из связывания нулевого полинома с Witt-полиномом, тождественно равен нулю.

LaTeX

$$$$\bind_1(0,\mathrm{wittPolynomial}(p,R,n)) = 0.$$$$

Lean4

/-- The function that is constantly zero on Witt vectors is a polynomial function. -/
instance zeroIsPoly [Fact p.Prime] : IsPoly p fun _ _ _ => 0 :=
  ⟨⟨0, by intros; funext n; simp only [Pi.zero_apply, map_zero, zero_coeff]⟩⟩

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