coeff_smul — Mathlib

English

Taking a scalar multiple commutes with taking coefficients: coeff m (C • p) = C • coeff m p.

Русский

Умножение на скаляр и взятие коэффициентов совместимы: coeff m (C • p) = C • coeff m p.

LaTeX

$$$\forall m\ C\ (p):\ \mathrm{coeff}\;m (C \cdot p) = C \cdot \mathrm{coeff}\;m\;p$$$

Lean4

@[simp]
theorem coeff_smul {S₁ : Type*} [SMulZeroClass S₁ R] (m : σ →₀ ℕ) (C : S₁) (p : MvPolynomial σ R) :
    coeff m (C • p) = C • coeff m p :=
  smul_apply C p m

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