monomial_mul — Mathlib

English

Product of two monomials is the monomial corresponding to the sum of their exponent vectors and the product of their coefficients.

Русский

Произведение двух мономов даёт мономом, чья экспонента равна сумме экспонент, а коэффициент — произведение исходных коэффициентов.

LaTeX

$$$\mathrm{monomial}(s,a) \cdot \mathrm{monomial}(s',b) = \mathrm{monomial}(s+s', ab)$$$

Lean4

@[simp]
theorem monomial_mul {s s' : σ →₀ ℕ} {a b : R} : monomial s a * monomial s' b = monomial (s + s') (a * b) :=
  AddMonoidAlgebra.single_mul_single ..

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