weightedHomogeneousComponent_C_mul

English

Multiplication by a constant on φ commutes with taking the n-th weighted homogeneous component.

Русский

Умножение полинома на константу C r коммутирует с взвешенной однородной компонентой степени n.

LaTeX

$$$weightedHomogeneousComponent\, w\, n\, (C\, r\cdot \varphi) = C\, r\cdot weightedHomogeneousComponent\, w\, n\, \varphi$$$

Lean4

@[simp]
theorem weightedHomogeneousComponent_C_mul (n : M) (r : R) :
    weightedHomogeneousComponent w n (C r * φ) = C r * weightedHomogeneousComponent w n φ := by
  simp only [C_mul', LinearMap.map_smul]

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