ofFinsupp_sub — Mathlib

English

The polynomial representing the difference of two coefficient sequences is the difference of the corresponding polynomials: ⟨a - b⟩ = ⟨a⟩ - ⟨b⟩.

Русский

Полином, соответствующий разности двух последовательностей коэффициентов, равен разности соответствующих полиномов: ⟨a - b⟩ = ⟨a⟩ - ⟨b⟩.

LaTeX

$$$\langle a - b \rangle = \langle a \rangle - \langle b \rangle.$$$

Lean4

@[simp]
theorem ofFinsupp_sub {R : Type u} [Ring R] {a b} : (⟨a - b⟩ : R[X]) = ⟨a⟩ - ⟨b⟩ :=
  by
  rw [sub_eq_add_neg, ofFinsupp_add, ofFinsupp_neg]
  rfl

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