smulCommClass_symm_self — Mathlib

English

If SMulCommClass k R k holds, then the symmetric smul-commutativity extends to AddMonoidAlgebra k G.

Русский

Если SMulCommClass k R k верно, то симметричное smul‑commutativity распространяется на AddMonoidAlgebra k G.

LaTeX

$$$$\text{SMulCommClass } k[G]\ R\ k[G].$$$$

Lean4

instance smulCommClass_symm_self [SMulCommClass k R k] : SMulCommClass k[G] R k[G] :=
  @MonoidAlgebra.smulCommClass_symm_self k (Multiplicative G) R _ _ _ _

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