English
If S is a Monoid and acts on R via MulAction, then QuadraticAlgebra R a b carries a natural MulAction of S, with one_smul and mul_smul laws.
Русский
Пусть S — моноид и действует на R посредством умножения. Тогда квадратическая алгебра QuadraticAlgebra R a b наследует естественное действие S, удовлетворяющее правилам one_smul и mul_smul.
LaTeX
$$$MulAction S (QuadraticAlgebra R a b)$$$
Lean4
instance [Monoid S] [MulAction S R] : MulAction S (QuadraticAlgebra R a b)
where
one_smul _ := by ext <;> simp
mul_smul _ _ _ := by ext <;> simp [mul_smul]