gradedMonoid — Mathlib

English

The product ι_Q(m) ι_Q(m) equals the scalar Q(m) inside the appropriate algebra map, i.e., ι_Q(m)² = algebraMap(Q(m)) in the direct sum representation.

Русский

Произведение ι_Q(m) на себя равно скаляру Q(m) внутри соответствующего отображения алгебры: ι_Q(m)² = algebraMap(Q(m)).

LaTeX

$$$ι_Q(m) \\cdot ι_Q(m) = algebraMap\\, R\\, (Q(m))$$$

Lean4

instance gradedMonoid : SetLike.GradedMonoid (evenOdd Q)
    where
  one_mem := Submodule.one_le.mp (one_le_evenOdd_zero Q)
  mul_mem _i _j _p _q hp hq := Submodule.mul_le.mp (evenOdd_mul_le Q _ _) _ hp _ hq

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