instSMulCommClassSubtypeMem_1 — Mathlib

English

If we have a Submonoid S inside a monoid, then there is a natural SMulCommClass structure on the subtype of S, inherited from the larger action.

Русский

Для подмоноида внутри мономида существует естественная структура SMulCommClass на подтипе S, наследуемая от большего действия.

LaTeX

$$$ \\text{instance } (SMulCommClass)\\; (Subtype\\; (\\lambda x, x \\in S)) \\; β $$$

Lean4

@[to_additive]
instance (priority := low) [SMul α β] [SMul M' β] [SMulCommClass α M' β] : SMulCommClass α s β :=
  ⟨fun a s => smul_comm a (s : M')⟩

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