mul_mem_graded — Mathlib

English

If gi ∈ A_i and gj ∈ A_j in a graded set, then the product gi gj lies in A_{i+j}.

Русский

Если элементы gi и gj принадлежат соответствующим градациям A_i и A_j, то их произведение принадлежит A_{i+j}.

LaTeX

$$$$\forall i,j,\; gi \in A_i \land gj \in A_j \Rightarrow gi \cdot gj \in A_{i+j}.$$$$

Lean4

theorem mul_mem_graded {S : Type*} [SetLike S R] [Mul R] [Add ι] {A : ι → S} [SetLike.GradedMul A] ⦃i j⦄ {gi gj}
    (hi : gi ∈ A i) (hj : gj ∈ A j) : gi * gj ∈ A (i + j) :=
  SetLike.GradedMul.mul_mem hi hj

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