isScalarTower — Mathlib

English

Given compatible scalar actions across T, S, R and modules M, the canonical construction tsze R M inherits an IsScalarTower structure from Prod.

Русский

Пусть заданы совместные действия скаляров T, S и R на R и M; конструкция tsze R M наследует структуру IsScalarTower.

LaTeX

$$IsScalarTower T S (tsze R M)$$

Lean4

instance isScalarTower [SMul T R] [SMul T M] [SMul S R] [SMul S M] [SMul T S] [IsScalarTower T S R]
    [IsScalarTower T S M] : IsScalarTower T S (tsze R M) :=
  Prod.isScalarTower

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