leftInverse_trunc_toLaurent — Mathlib

English

trunc is a left inverse to Polynomial.toLaurent; in particular, for every polynomial f ∈ R[X], trunc (toLaurent f) = f.

Русский

trunc является левым обратным toLaurent; в частности, для любого полинома f ∈ R[X], trunc(toLaurent f) = f.

LaTeX

$$$\forall f \in R[X]:\ trunc(\text{toLaurent} f) = f$$$

Lean4

@[simp]
theorem leftInverse_trunc_toLaurent : Function.LeftInverse (trunc : R[T;T⁻¹] → R[X]) Polynomial.toLaurent :=
  by
  refine fun f => f.induction_on' ?_ ?_
  · intro f g hf hg
    simp only [hf, hg, map_add]
  · intro n r
    simp only [Polynomial.toLaurent_C_mul_T, trunc_C_mul_T, Int.natCast_nonneg, Int.toNat_natCast, if_true]

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