instIsScalarTower — Mathlib

English

If there is a scalar tower M N X, then there is a scalar tower M N (SeparationQuotient X).

Русский

Если существует каскад скаляров M→N→X, то существует и каскад скаляров на SeparationQuotient X.

LaTeX

$$IsScalarTower M N (SeparationQuotient X)$$

Lean4

@[to_additive]
instance instIsScalarTower [SMul M N] [ContinuousConstSMul N X] [IsScalarTower M N X] :
    IsScalarTower M N (SeparationQuotient X) where
  smul_assoc a b := surjective_mk.forall.2 fun x ↦ congr_arg mk <| smul_assoc a b x

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