toFinsupp_mul — Mathlib

English

For polynomials a, b over a semiring, the finsupp embedding respects multiplication: (a · b).toFinsupp = a.toFinsupp · b.toFinsupp.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toFinsupp_mul (a b : R[X]) : (a * b).toFinsupp = a.toFinsupp * b.toFinsupp := by rw [← ofFinsupp_mul]

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