single_order_mul_powerSeriesPart — Mathlib

English

For a Laurent series x, multiplying powerSeriesPart by a single term recovers x: (single x.order 1) * x.powerSeriesPart = x.

Русский

Умножение powerSeriesPart на единичный член с порядком x восстанавливает x: (single x.order 1) * x.powerSeriesPart = x.

LaTeX

$$$(\text{single}(\mathrm{order}(x),1) : R⟨⟨X⟧⟩) \cdot x.powerSeriesPart = x$$$

Lean4

@[simp]
theorem single_order_mul_powerSeriesPart (x : R⸨X⸩) : (single x.order 1 : R⸨X⸩) * x.powerSeriesPart = x :=
  by
  ext n
  rw [← sub_add_cancel n x.order, coeff_single_mul_add, sub_add_cancel, one_mul]
  by_cases h : x.order ≤ n
  ·
    rw [Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h), coeff_coe_powerSeries, powerSeriesPart_coeff, ←
      Int.eq_natAbs_of_nonneg (sub_nonneg_of_le h), add_sub_cancel]
  · rw [ofPowerSeries_apply, embDomain_notin_range]
    · contrapose! h
      exact order_le_of_coeff_ne_zero h.symm
    · contrapose! h
      simp only [Set.mem_range, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk] at h
      cutsat

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