instMulAction — Mathlib

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]

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