instIsScalarTower — Mathlib

English

The weak space forms a scalar tower with respect to an auxiliary semiring 𝕝, compatible with the original scalars 𝕜.

Русский

Слабое пространство образует тензорную структуру над дополнительной полусетью 𝕝, совместимую с начальными скалярами 𝕜.

LaTeX

$$$IsScalarTower\\ 𝕝\\ 𝕜\\ (WeakSpace 𝕜 E)$$$

Lean4

instance instIsScalarTower [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
    IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E) :=
  WeakBilin.instIsScalarTower (topDualPairing 𝕜 E).flip

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