English
If S is star-closed (i.e., closed under star) and closed under the scalar action of R in a star R-module, then the subset S carries a natural structure of a star R-module (the subtype inherits the star action and scalar action).
Русский
Если S является звёздно замкнутым подмножеством в звёздном модуле над R и замкнуто по действию скаляра R, тогда S наследует естественную структуру звёздного R-модуля.
LaTeX
$$$\\forall r \\in R, \\forall x \\in S,\\; \\star(r \\cdot x) = (\\star r) \\cdot \\star x$$$
Lean4
/-- In a star `R`-module (i.e., `star (r • m) = (star r) • m`) any star-closed subset which is also
closed under the scalar action by `R` is itself a star `R`-module. -/
instance instStarModule {S : Type*} (R : Type*) {M : Type*} [Star R] [Star M] [SMul R M] [StarModule R M] [SetLike S M]
[SMulMemClass S R M] [StarMemClass S M] (s : S) : StarModule R s where star_smul _ _ := Subtype.ext <| star_smul _ _
