constantCoeff_wittPolynomial — Mathlib

English

If p is prime, then the constant coefficient of the Witt polynomial wittPolynomial p R n is zero for every n.

Русский

Если p — простое число, то константный коэффициент Witt-полины wittPolynomial p R n равен нулю для любого n.

LaTeX

$$$ \operatorname{constantCoeff}( wittPolynomial\ p\ R\ n ) = 0 $$$

Lean4

@[simp]
theorem constantCoeff_wittPolynomial [hp : Fact p.Prime] (n : ℕ) : constantCoeff (wittPolynomial p R n) = 0 :=
  by
  simp only [wittPolynomial, map_sum, constantCoeff_monomial]
  rw [sum_eq_zero]
  rintro i _
  rw [if_neg]
  rw [Finsupp.single_eq_zero]
  exact ne_of_gt (pow_pos hp.1.pos _)

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