smulCommClass_right — Mathlib

English

If SMul α β, SMul M' β and SMulCommClass α M' β, then the induced SMulCommClass on the Submonoid S' acting on β holds.

Русский

Если SMul α β и SMul M' β, а также SMulCommClass α M' β, то соответствующее свойство перенесётся на действие S' на β.

LaTeX

$$$\text{SMulCommClass } α\, S'\, β$ under the given hypotheses.$$

Lean4

@[to_additive]
instance smulCommClass_right [SMul α β] [SMul M' β] [SMulCommClass α M' β] (S : Submonoid M') : SMulCommClass α S β :=
  inferInstance

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