C_mul_monomial — Mathlib

English

Multiplying a constant polynomial C(a) by the monomial monomial(n,b) yields monomial(n, a b).

Русский

Умножение константного полинома C(a) на мономиал monomial(n,b) даёт monomial(n, a b).

LaTeX

$$$ C(a) \cdot \operatorname{monomial}(n,b) = \operatorname{monomial}(n, a b). $$$

Lean4

@[simp]
theorem C_mul_monomial : C a * monomial n b = monomial n (a * b) := by
  simp only [← monomial_zero_left, monomial_mul_monomial, zero_add]

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