isScalarTower — Mathlib

English

There is a scalar-tower structure: if N acts on R and O acts on R with an IsScalarTower N O R, then this induces IsScalarTower N O (MonoidAlgebra R M).

Русский

Существует структура башни скаляров: если N действует на R и O действует на R с IsScalarTower N O R, то это порождает IsScalarTower N O (MonoidAlgebra R M).

LaTeX

$$$\\text{IsScalarTower } N\\ O\\ (MonoidAlgebra\\ R\\ M)$$$

Lean4

@[to_additive (dont_translate := N) isScalarTower]
instance isScalarTower [SMulZeroClass N R] [SMulZeroClass O R] [SMul N O] [IsScalarTower N O R] :
    IsScalarTower N O (MonoidAlgebra R M) :=
  Finsupp.isScalarTower ..

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