ofFn_comp_toFn_eq_id_of_natDegree_lt

English

If a polynomial p has natDegree less than n, then composing ofFn with toFn recovers p: ofFn n (toFn n p) = p.

Русский

Если p имеет natDegree < n, то ofFn n (toFn n p) = p.

LaTeX

$$$\text{If } p.natDegree < n, \; \operatorname{ofFn}(n)(\operatorname{toFn}(n)(p)) = p.$$$

Lean4

theorem ofFn_comp_toFn_eq_id_of_natDegree_lt {n : ℕ} {p : R[X]} (h_deg : p.natDegree < n) : ofFn n (toFn n p) = p :=
  by
  ext i
  by_cases h : i < n
  · simp [h, toFn]
  · have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt <| by cutsat
    simp_all

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