coe_decompose_mul_of_left_mem — Mathlib

English

In a graded setting, the product of sums respects the direct-sum decomposition; the coefficient at degree n is a sum of pairwise components from degrees i and n-i.

Русский

В градуированной структуре произведение сумм в разложении по степеням имеет коэффициент степени n как сумма компонент степеней i и n-i.

LaTeX

$$$decompose 𝒜(a b) n = \,\sum_{i+j=n} (a_i)(b_j)$, with proper identifications.$$

Lean4

theorem coe_decompose_mul_of_left_mem (n) [Decidable (i ≤ n)] (a_mem : a ∈ 𝒜 i) :
    (decompose 𝒜 (a * b) n : A) = if i ≤ n then a * decompose 𝒜 b (n - i) else 0 :=
  by
  lift a to 𝒜 i using a_mem
  rw [decompose_mul, decompose_coe, coe_of_mul_apply]

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