smulCommClass_self — Mathlib

English

If SMulCommClass R k k holds, then there is SMulCommClass R (AddMonoidAlgebra k G) (AddMonoidAlgebra k G).

Русский

Если SMulCommClass R k k верно, то существует SMulCommClass R (AddMonoidAlgebra k G) (AddMonoidAlgebra k G).

LaTeX

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

Lean4

/-- Note that if `k` is a `CommSemiring` then we have `SMulCommClass k k k` and so we can take
`R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication. -/
instance smulCommClass_self [SMulCommClass R k k] : SMulCommClass R k[G] k[G] :=
  @MonoidAlgebra.smulCommClass_self k (Multiplicative G) R _ _ _ _

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