monomial_mul_monomial — Mathlib

English

The product of two monomials is a monomial with the sum of indices and product of coefficients: monomial(n,r) monomial(m,s) = monomial(n+m, rs).

Русский

Произведение двух мономиалов равно мономиалу с суммой степеней и произведением коэффициентов.

LaTeX

$$$\operatorname{monomial}(n,r) \cdot \operatorname{monomial}(m,s) = \operatorname{monomial}(n+m, rs)$$$

Lean4

theorem monomial_mul_monomial (n m : ℕ) (r s : R) : monomial n r * monomial m s = monomial (n + m) (r * s) :=
  toFinsupp_injective <| by simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]

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