coe_decompose_mul_add_of_right_mem

English

The decomposition map preserves multiplication in each homogeneous coordinate.

Русский

Разложение сохраняет умножение в каждой однородной координате.

LaTeX

$$$ DecomposeMul 𝒜 (x y) = DecomposeMul 𝒜 x \cdot DecomposeMul 𝒜 y. $$$

Lean4

theorem coe_decompose_mul_add_of_right_mem [AddRightCancelMonoid ι] [GradedRing 𝒜] {a b : A} (b_mem : b ∈ 𝒜 j) :
    (decompose 𝒜 (a * b) (i + j) : A) = decompose 𝒜 a i * b :=
  by
  lift b to 𝒜 j using b_mem
  rw [decompose_mul, decompose_coe, coe_mul_of_apply_add]

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