coe_decompose_mul_of_right_mem_zero

English

If b ∈ 𝒜 0, then (a*b) and decompose agree on the 0-th component via right-multiplication by b.

Русский

Если b ∈ 𝒜 0, то (a*b) и разложение совпадают на нулевой координате через умножение справа на b.

LaTeX

$$$ (decompose 𝒜 (a * ↑b) i : A) = decompose 𝒜 a i * b, \text{ with } b ∈ 𝒜 0. $$$

Lean4

theorem coe_decompose_mul_of_right_mem_zero [AddMonoid ι] [GradedRing 𝒜] {a b : A} (b_mem : b ∈ 𝒜 0) :
    (decompose 𝒜 (a * b) i : A) = decompose 𝒜 a i * b :=
  by
  lift b to 𝒜 0 using b_mem
  rw [decompose_mul, decompose_coe, coe_mul_of_apply_of_mem_zero]

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