negIsPoly — Mathlib

English

The additive negation is a polynomial function on Witt vectors.

Русский

Аддитивное отрицание является полиномиальной функцией Witt-векторов.

LaTeX

$$$$IsPoly_p(\operatorname{Neg.neg}).$$$$

Lean4

/-- The additive negation is a polynomial function on Witt vectors. -/
instance negIsPoly [Fact p.Prime] : IsPoly p fun R _ => @Neg.neg (𝕎 R) _ :=
  ⟨⟨fun n => rename Prod.snd (wittNeg p n), by
      intros; funext n
      rw [neg_coeff, aeval_eq_eval₂Hom, eval₂Hom_rename]
      apply eval₂Hom_congr rfl _ rfl
      ext ⟨i, k⟩; fin_cases i; rfl⟩⟩

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