wittMul_zero — Mathlib

English

The Witt multiplication at index 0 is X(0,0) · X(1,0).

Русский

Witt умножение на индексе 0 равно X(0,0) · X(1,0).

LaTeX

$$$$ \mathrm{wittMul}(p,0) = X(0,0) \cdot X(1,0). $$$$

Lean4

@[simp]
theorem wittMul_zero : wittMul p 0 = X (0, 0) * X (1, 0) :=
  by
  apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
  simp only [wittMul, wittStructureRat, rename_X, xInTermsOfW_zero, map_X, wittPolynomial_zero, map_mul, bind₁_X_right,
    map_wittStructureInt]

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