trunc_one_left — Mathlib

English

For any power series p, the truncation at level 1 equals the constant term of p, regarded as a constant power series.

Русский

Для любой степенной серии p усечение на уровне 1 равно константной части p, рассматриваемой как константная степенная серия.

LaTeX

$$$\\forall p : R\\lbrace\\lbrace X \\rbrace\\rbrace, \\; \\operatorname{trunc}(1)\\, p = .C(\\operatorname{coeff} 0\\, p)$$$

Lean4

@[simp]
theorem trunc_one_left (p : R⟦X⟧) : trunc (R := R) 1 p = .C (coeff 0 p) := by ext i;
  simp +contextual [coeff_trunc, Polynomial.coeff_C]

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