instSMulCommClass — Mathlib

English

There is a SMulCommClass structure on the quotient c.Quotient, ensuring that the actions of α and β commute on the quotient, given the appropriate towers and compatibilities.

Русский

Для фактор-модуля c.Quotient существует структура SMulCommClass, обеспечивающая взаимную коммутативность действий α и β на факторе.

LaTeX

$$SMulCommClass α β c.Quotient$$

Lean4

instance instSMulCommClass {α β M : Type*} [MulOneClass M] [SMul α M] [SMul β M] [IsScalarTower α M M]
    [IsScalarTower β M M] [SMulCommClass α β M] (c : Con M) : SMulCommClass α β c.Quotient where
  smul_comm a b := Quotient.ind' fun m => congr_arg Quotient.mk'' <| smul_comm a b m

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