bind₁_onePoly_wittPolynomial — Mathlib

English

Binding the Witt polynomial with the constant-one polynomial yields the constant one polynomial.

Русский

Связывание Witt-полинома с однополиным приходят к единичному константному полиному.

LaTeX

$$$$\bind_1(\mathrm{onePoly}, \mathrm{wittPolynomial}(p,\mathbb{Z},n)) = 1.$$$$

Lean4

@[simp]
theorem bind₁_onePoly_wittPolynomial [hp : Fact p.Prime] (n : ℕ) : bind₁ onePoly (wittPolynomial p ℤ n) = 1 :=
  by
  rw [wittPolynomial_eq_sum_C_mul_X_pow, map_sum, Finset.sum_eq_single 0]
  · simp only [onePoly, one_pow, one_mul, map_pow, C_1, pow_zero, bind₁_X_right, if_true]
  · intro i _hi hi0
    simp only [onePoly, if_neg hi0, zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, map_pow, bind₁_X_right, map_mul]
  · simp

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