coeff_truncateFun — Mathlib

English

For any x ∈ 𝕎R and i ∈ Fin n, the i-th coefficient of truncateFun n x equals the i-th coefficient of x.

Русский

Для любого x ∈ 𝕎R и i ∈ Fin n i-й коэффициент усечённого виттового вектора равен i-му коэффициенту x.

LaTeX

$$$ (\mathrm{truncateFun}(n)(x)).\mathrm{coeff} i = x.\mathrm{coeff} i $$$

Lean4

@[simp]
theorem coeff_truncateFun (x : 𝕎 R) (i : Fin n) : (truncateFun n x).coeff i = x.coeff i := by
  rw [truncateFun, TruncatedWittVector.coeff_mk]

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