English
If the scalar product forms a MulAction, then p carries a MulAction of S by restricting the ambient action: for s ∈ S and x ∈ p, s • x ∈ p and the action is given by the ambient action restricted to p.
Русский
Если скалярное произведение образует действие MulAction, то p наследует действие S путём ограничения действием над M: для s ∈ S и x ∈ p выполняется s • x ∈ p, и это действие получается путём ограничения действия над p.
LaTeX
$$$ \\forall s : S, \\forall x : p,\\ s \\cdot x \\in p \\ \\\\and\\ \\ (s \\cdot x) = s \\cdot x $ (inherited from M)$$
Lean4
/-- If the scalar product forms a `MulAction`, then the subset inherits this action -/
@[to_additive]
instance mulAction' : MulAction S p where
smul := (· • ·)
one_smul x := Subtype.ext <| one_smul _ (x : M)
mul_smul c₁ c₂ x := Subtype.ext <| mul_smul c₁ c₂ (x : M)
