instIsScalarTower_1 — Mathlib

English

If P, S, R have appropriate modules and algebra structures, then IsScalarTower P (WithVal v) S holds.

Русский

Если имеются соответствующие модули и алгебраические структуры, то IsScalarTower P (WithVal v) S выполняется.

LaTeX

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

Lean4

instance {P S : Type*} [Ring S] [Semiring P] [Module P R] [Module P S] [Algebra R S] [IsScalarTower P R S] :
    IsScalarTower P (WithVal v) S :=
  inferInstanceAs (IsScalarTower P R S)

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