isScalarTower — Mathlib

English

If S, T act on R and M with consistent scalar towers, then S and T induce a scalar tower on the quotient M/P: (S, T) acts on M/P satisfying the associativity of scalars: (s · t) · [x] = s · (t · [x]).

Русский

Если S и T действуют на R и M, образуя совместную «башню scalar tower», то эта башня поднимается на фактор-модуль M/P: (s · t) · [x] = s · (t · [x]).

LaTeX

$$$\forall s \in S, \forall t \in T,\ (s\,t) \cdot [x] = s \cdot (t \cdot [x])$$$

Lean4

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

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