smul_monomial

Mathlib.Algebra.MvPolynomial.Basic

URI: https://scilib.ai/kg/mathlib#MvPolynomial.smul_monomial

English

Scalar multiplication coincides with multiplication by a constant: a • p = C a * p.

Русский

Умножение на скаляр совпадает с умножением на константу: a • p = C a * p.

LaTeX

$$$ a \cdot p = C a * p $$$

Lean4

theorem smul_monomial {S₁ : Type*} [SMulZeroClass S₁ R] (r : S₁) : r • monomial s a = monomial s (r • a) :=
  Finsupp.smul_single _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru