mul_charP_coeff_zero — Mathlib

English

In a CharP ring, multiplying a Witt vector by p yields a Witt vector whose 0-th coefficient is 0: (x · p).coeff 0 = 0.

Русский

В кольце с характеристикой p умножение Witt-вектора на p даёт Witt-вектор с нулевым нулевым коэффициентом: (x · p).coeff 0 = 0.

LaTeX

$$$ (x \cdot p).coeff 0 = 0 $$$

Lean4

theorem mul_charP_coeff_zero [CharP R p] (x : 𝕎 R) : (x * p).coeff 0 = 0 := by
  rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero, zero_pow hp.out.ne_zero]

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