coe_decompose_mul_of_right_mem_of_le

English

Given a family of submodules M(i) forming a graded monoid, one can equip A with a graded algebra structure via the internal direct sum construction.

Русский

Дана семья подмодулей M(i), образующая градуированную моноиду; через внутреннее прямое сумма A получает структуру градуированной алгебры.

LaTeX

$$$\text{If } M: ι \to \text{Submodule}(R,A) \text{ with } SetLike.GradedMonoid\ M, \text{ then }\mathrm{gradedAlgebra}(hM):=\text{GradedAlgebra } M.$$$

Lean4

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

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