instDistribMulAction — Mathlib

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

Похожие утверждения