v2_coeff — Mathlib

English

In the 2-component Witt vector [x,y], the i-th coefficient equals the i-th coordinate of the pair (x,y) for i ∈ Fin 2.

Русский

В 2-компонентном Witt-векторе [x,y] i-я координата равна i-й координате пары (x,y) при i ∈ Fin 2.

LaTeX

$$$$ (![x,y]\,i).\mathrm{coeff} = ![x.\mathrm{coeff}, y.\mathrm{coeff}]\,i \quad (i \in \mathrm{Fin}\,2). $$$$

Lean4

@[simp]
theorem v2_coeff {p' R'} (x y : WittVector p' R') (i : Fin 2) : (![x, y] i).coeff = ![x.coeff, y.coeff] i := by
  fin_cases i <;> simp

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