toFinsupp_sub — Mathlib

English

For polynomials a, b over a ring, the finsupp embedding respects subtraction: (a − b).toFinsupp = a.toFinsupp − b.toFinsupp.

Русский

Для полиномов a, b над кольцом отображение toFinsupp сохраняет вычитание: (a − b).toFinsupp = a.toFinsupp − b.toFinsupp.

LaTeX

$$$(a - b)^{\\wedge} = a^{\\wedge} - b^{\\wedge}$$$

Lean4

@[simp]
theorem toFinsupp_sub {R : Type u} [Ring R] (a b : R[X]) : (a - b).toFinsupp = a.toFinsupp - b.toFinsupp :=
  by
  rw [sub_eq_add_neg, ← toFinsupp_neg, ← toFinsupp_add]
  rfl

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