instIsScalarTower — Mathlib

English

There is a scalar tower IsScalarTower R S (⨁ i, M_i) when each M_i is an R-module and also an S-module compatibly with R.

Русский

Существует тетраскалярная башня IsScalarTower R S (⨁ i, M_i), когда каждый M_i является модулем над R и над S совместимо с R.

LaTeX

$$$\\mathrm{IsScalarTower}\\; R\\; S\\; (\\bigoplus_{i} M_i).$$$

Lean4

instance {S : Type*} [Semiring S] [SMul R S] [∀ i, Module S (M i)] [∀ i, IsScalarTower R S (M i)] :
    IsScalarTower R S (⨁ i, M i) :=
  DFinsupp.isScalarTower

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