ofFinsupp_mul — Mathlib

English

The coefficient sequence of the product corresponds to the product of the coefficient sequences: ⟨a · b⟩ = ⟨a⟩ · ⟨b⟩.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ofFinsupp_mul (a b) : (⟨a * b⟩ : R[X]) = ⟨a⟩ * ⟨b⟩ :=
  show _ = mul _ _ by rw [mul_def]

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