coe_decompose_mul_of_right_mem — Mathlib

English

The decomposition map distributes over addition and multiplication in accordance with the grading, preserving homogeneous components.

Русский

Разложение распределяется по сложению и умножению в соответствии с градацией, сохраняющей однородные компоненты.

LaTeX

$$$decompose 𝒜 (a + b) = decompose 𝒜 a + decompose 𝒜 b$, and similarly for products, componentwise.$$

Lean4

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

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