coe_decompose_mul_of_left_mem_of_le

English

If a and b are homogeneous of degrees i and j respectively, then the degree n component of a*b is controlled by i+j and vanishes when n < i or n < j appropriately; explicit formulas separate left and right cases.

Русский

Если a и b однородны степеней i и j, то компонент степени n умножения зависит от i+j и исчезает при несоответствии требований; формулы разделяют лево и право.

LaTeX

$$Provisions for proj decompositions with cases i ≤ n or i > n, giving expressions in terms of a, b, and their components.$$

Lean4

theorem coe_decompose_mul_of_left_mem_of_le (a_mem : a ∈ 𝒜 i) (h : i ≤ n) :
    (decompose 𝒜 (a * b) n : A) = a * decompose 𝒜 b (n - i) :=
  by
  lift a to 𝒜 i using a_mem
  rwa [decompose_mul, decompose_coe, coe_of_mul_apply_of_le]

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