instSMulCommClassSubtypeMem_1 — Mathlib

English

If α's action is commutative with respect to M and N, then the induced action on the subtype s is also commutative: a·b·x = b·a·x for a ∈ M, b ∈ N, x ∈ s.

Русский

Если действие α совместно по умолчанию относительно M и N, то для подтипа s получаемое действие тоже коммутативно: a·b·x = b·a·x для a ∈ M, b ∈ N, x ∈ s.

LaTeX

$$$\\forall a \\in M, \\forall b \\in N, \\forall x \\in s:\\; a \\cdot (b \\cdot x) = b \\cdot (a \\cdot x)$$$

Lean4

@[to_additive]
instance (priority := 50) [SMulCommClass M N α] : SMulCommClass M N s where
  smul_comm _ _ _ := Subtype.ext (smul_comm ..)

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