instIsScalarTower — Mathlib

English

If there is a scalar tower K → K' → V acting on V, then there is a corresponding IsScalarTower K → K' → WithLp p V.

Русский

Если существует скалярная башня K → K' → V, действующая на V, то существует соответствующая башня IsScalarTower K → K' → WithLp p V.

LaTeX

$$$IsScalarTower K K' V \Rightarrow IsScalarTower K K' (WithLp p V)$$$

Lean4

@[to_additive]
instance instIsScalarTower [SMul K K'] [SMul K V] [SMul K' V] [IsScalarTower K K' V] :
    IsScalarTower K K' (WithLp p V) :=
  ‹IsScalarTower K K' V›

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