instIsScalarTower — Mathlib

English

If M, N, α form a scalar-tower relation, then the same tower property holds when M is replaced by its order dual, i.e., the scalar-tower condition is preserved under taking the order dual on the left factor.

Русский

Если M, N, α образуют цепь скалярного действия, то та же цепь свойств сохраняется при замене левого множителя M на его порядок-двойник, т.е. цепь скалярного действия сохраняется при переходе к порядковому двойнику слева.

LaTeX

$$$ \\text{IsScalarTower}(M,N,\\alpha) \\Rightarrow \\text{IsScalarTower}(M^{\\mathrm{op}},N,\\alpha). $$$

Lean4

@[to_additive]
instance instIsScalarTower [SMul M N] [SMul M α] [SMul N α] [IsScalarTower M N α] : IsScalarTower Mᵒᵈ N α :=
  ‹IsScalarTower M N α›

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