smulMemClass — Mathlib

English

StarSubalgebra carries an SMulMemClass structure, i.e., smul by scalars preserves the subalgebra.

Русский

StarSubalgebra имеет структуру SMulMemClass: умножение на скаляры сохраняет подалгебру.

LaTeX

$$$\\text{SMulMemClass}(\\text{StarSubalgebra }R A, R, A)$$$

Lean4

instance smulMemClass : SMulMemClass (StarSubalgebra R A) R A where
  smul_mem {s} r a (ha : a ∈ s.toSubalgebra) := (SMulMemClass.smul_mem r ha : r • a ∈ s.toSubalgebra)

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