trunc_coe_eq_self — Mathlib

English

If a polynomial f has natDegree f < n, then the truncation of its power-series embedding equals f.

Русский

Если многочлен f имеет natDegree f < n, то усечение его отображения в power-series равно f.

LaTeX

$$$\\forall f : R[X], \\; \\operatorname{natDegree} f < n \\Rightarrow \\operatorname{trunc} n (f : R\\langle\\langle X \\rangle\\rangle) = f$$$

Lean4

theorem trunc_coe_eq_self {n} {f : R[X]} (hn : natDegree f < n) : trunc n (f : R⟦X⟧) = f :=
  by
  rw [← Polynomial.coe_inj]
  ext m
  rw [coeff_coe, coeff_trunc]
  split
  case isTrue h => rfl
  case isFalse h =>
    rw [not_lt] at h
    rw [coeff_coe]; symm
    exact coeff_eq_zero_of_natDegree_lt <| lt_of_lt_of_le hn h

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