instSMulCommClass — Mathlib

English

There is a commuting scalar action of α with submodules: the scalar action commutes with multiplication of submodules, i.e., a • (S * T) = (a • S) * T = S * (a • T).

Русский

Скалярное действие α согласуется с умножением подмодулов: a • (S * T) = (a • S) * T = S * (a • T).

LaTeX

$$$a \\cdot (S \\cdot T) = (a \\cdot S) \\cdot T = S \\cdot (a \\cdot T)$$$

Lean4

instance [SMulCommClass α A A] : SMulCommClass α (Submodule R A) (Submodule R A) where
  smul_comm a S
    T := by
    rw [← S.span_eq, ← T.span_eq, smul_span, smul_eq_mul, smul_eq_mul, span_mul_span, span_mul_span, smul_span,
      mul_smul_comm]

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