instIsScalarTower — Mathlib

English

Under suitable hypotheses, the tower P → S → WithVal v forms a scalar tower: IsScalarTower P S (WithVal v).

Русский

При надлежащих условиях пирамидальная структура P → S → WithVal v образует скалярную башню: IsScalarTower P S (WithVal v).

LaTeX

$$$IsScalarTower P S (WithVal v)$$$

Lean4

instance [Ring R] [SMul P S] [SMul S R] [SMul P R] [IsScalarTower P S R] (v : Valuation R Γ₀) :
    IsScalarTower P S (WithVal v) :=
  inferInstanceAs (IsScalarTower P S R)

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