smulCommClass_left — Mathlib

English

If SMul α β, SMul M' α, SMul M' β and SMulCommClass M' α β hold, then the induced SMulCommClass on the Submonoid S' (via SetLike membership) also holds.

Русский

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

LaTeX

$$$\text{SMulCommClass } S'\, α\, β$ given that $SMul α β$, $SMul M' α$, $SMul M' β$ и $SMulCommClass M' α β$.$$

Lean4

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

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