smul_monomial — Mathlib

English

Scalar action commutes with monomial: a • monomial(n,b) = monomial(n, a • b).

Русский

Действие скаляра на мономиал эквивалентно мономиалу с умноженным коэффициентом.

LaTeX

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

Lean4

theorem smul_monomial {S} [SMulZeroClass S R] (a : S) (n : ℕ) (b : R) : a • monomial n b = monomial n (a • b) :=
  toFinsupp_injective <| AddMonoidAlgebra.smul_single _ _ _

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