English
If a subset s of α is closed under the M–N–α action (i.e., there is a compatible SMulMemClass structure), then the subset carries a natural action of M when viewed as a subtype of α.
Русский
Если множество s ⊆ α замкнуто относительно действия M над α (существует совместимая структура SMulMemClass), то подмножество несет естественное действие M, считая его подтипом α.
LaTeX
$$$\\exists \\text{SMul on } s:\\, \\forall r \\in M, \\forall x=(a,ha) \\in s:\\; r \\cdot x = (r\\cdot a, \\text{smul\_mem}\\, ha)$$$
Lean4
/-- A subset closed under the scalar action inherits that action. -/
@[to_additive /-- A subset closed under the additive action inherits that action. -/
]
instance (priority := 50) smul' : SMul M s where smul r x := ⟨r • x.1, smul_one_smul N r x.1 ▸ smul_mem _ x.2⟩
