English
If S is a Monoid acting on an AddMonoid R with a distributive action, then QuadraticAlgebra R a b becomes a DistribMulAction: smul_zero and smul_add hold.
Русский
Если S — моноид, действующий на AddMonoid R распределённо, то QuadraticAlgebra R a b становится DistribMulAction: выполняются smul_zero и smul_add.
LaTeX
$$$DistribMulAction S (QuadraticAlgebra R a b)$$$
Lean4
instance [Monoid S] [AddMonoid R] [DistribMulAction S R] : DistribMulAction S (QuadraticAlgebra R a b)
where
smul_zero _ := by ext <;> simp
smul_add _ _ _ := by ext <;> simp