smulCommClass_left — Mathlib

English

Restriction of SMulCommClass to a subgroup: if SMulCommClass G α β holds, then SMulCommClass S α β holds for a subgroup S ≤ G.

Русский

Ограничение SMulCommClass к подпгруппе: если SMulCommClass G α β выполняется, тогда SMulCommClass S α β выполняется для подгруппы S ≤ G.

LaTeX

$$$\text{SMulCommClass}(S, \alpha, \beta)$$$

Lean4

@[to_additive]
instance smulCommClass_left [MulAction G β] [SMul α β] [SMulCommClass G α β] (S : Subgroup G) : SMulCommClass S α β :=
  S.toSubmonoid.smulCommClass_left

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