instSMulMemClass — Mathlib

English

An SMulMemClass instance is provided for NonUnitalStarSubalgebra, ensuring compatibility of scalar action with subalgebra membership.

Русский

Существование экземпляра SMulMemClass для NonUnitalStarSubalgebra обеспечивает совместимость действия скаляра со включением подалгебры.

LaTeX

$$$\\text{SMulMemClass }(\\text{NonUnitalStarSubalgebra } R A) R A$$$

Lean4

instance instSMulMemClass : SMulMemClass (NonUnitalStarSubalgebra R A) R A where smul_mem {s} := s.smul_mem'

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