monomial_mul_monomial — Mathlib

English

The product of two monomials is the monomial with summed degrees and multiplied coefficients: monomial m a · monomial n b = monomial (m+n) (a b).

Русский

Произведение двух мономов равно моному с суммой степеней и произведением коэффициентов: monomial m a · monomial n b = monomial (m+n) (a b).

LaTeX

$$$$ \operatorname{monomial}(m,a) \cdot \operatorname{monomial}(n,b) = \operatorname{monomial}(m+n, a b) $$$$

Lean4

theorem monomial_mul_monomial (m n : ℕ) (a b : R) : monomial m a * monomial n b = monomial (m + n) (a * b) := by
  simpa [monomial] using MvPowerSeries.monomial_mul_monomial (Finsupp.single () m) (Finsupp.single () n) a b

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