ofFinsupp_add — Mathlib

English

The polynomial corresponding to the sum of two coefficient sequences is the sum 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_add {a b} : (⟨a + b⟩ : R[X]) = ⟨a⟩ + ⟨b⟩ :=
  show _ = add _ _ by rw [add_def]

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