coeff_truncate — Mathlib

English

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

Русский

Для x ∈ 𝕎 R и i ∈ Fin n, i-й коэффициент в truncate n x равен i-й коэффициенту x.

LaTeX

$$$$ (\\operatorname{truncate}\n n\\ x).\\mathrm{coeff} i = x.\\mathrm{coeff} i, \\quad i:\\Fin n. $$$$

Lean4

@[simp]
theorem coeff_truncate (x : 𝕎 R) (i : Fin n) : (truncate n x).coeff i = x.coeff i :=
  coeff_truncateFun _ _

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