wittPolynomial_one — Mathlib

English

For any p and R, the first Witt polynomial is W_p,R,1 = C(p) X_1 + X_0^p.

Русский

Для любого p и R первый Witt-полином равен W_p,R,1 = C(p) X_1 + X_0^p.

LaTeX

$$$ wittPolynomial p R 1 = C (p : R) * X 1 + X 0 ^ p $$$

Lean4

@[simp]
theorem wittPolynomial_one : wittPolynomial p R 1 = C (p : R) * X 1 + X 0 ^ p := by
  simp only [wittPolynomial_eq_sum_C_mul_X_pow, sum_range_succ_comm, range_one, sum_singleton, one_mul, pow_one, C_1,
    pow_zero, tsub_self, tsub_zero]

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