smulCommClass — Mathlib

English

If S, T act on R and M with IsScalarTower structures and commute on M, then their actions commute on the quotient M/P: a ∈ S and b ∈ T satisfy a • (b • [x]) = b • (a • [x]).

Русский

Если S и T действуют на R и M с учётом структур IsScalarTower и их действия коммутируют на M, то их действия коммутируют и на фактор-модуле M/P: a • (b • [x]) = b • (a • [x]).

LaTeX

$$$\forall a \in S, \forall b \in T,\ a \cdot (b \cdot [x]) = b \cdot (a \cdot [x])$$$

Lean4

instance smulCommClass (T : Type*) [SMul T R] [SMul T M] [IsScalarTower T R M] [SMulCommClass S T M] :
    SMulCommClass S T (M ⧸ P) where smul_comm _x _y := Quotient.ind' fun _z => congr_arg mk (smul_comm _ _ _)

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