instIsScalarTower — Mathlib

English

Assume compatible scalar actions of 𝕝 and 𝕜 and an IsScalarTower 𝕝 ⊢ 𝕜 ⊢ WeakBilin B. Then WeakBilin B satisfies the IsScalarTower 𝕝 𝕜 (WeakBilin B).

Русский

Пусть имеются совместимые действия скаляров 𝕝 и 𝕜 и выполняется IsScalarTower 𝕝 ⊢ 𝕜 ⊢ WeakBilin B. Тогда WeakBilin B имеет структуру IsScalarTower 𝕝 𝕜 (WeakBilin B).

LaTeX

$$$IsScalarTower\ 𝕝\ 𝕜\ (WeakBilin B)$ under the given hypotheses.$$

Lean4

instance instIsScalarTower [CommSemiring 𝕜] [CommSemiring 𝕝] [AddCommMonoid E] [Module 𝕜 E] [AddCommMonoid F]
    [Module 𝕜 F] [SMul 𝕝 𝕜] [Module 𝕝 E] [s : IsScalarTower 𝕝 𝕜 E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
    IsScalarTower 𝕝 𝕜 (WeakBilin B) :=
  s

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