instIsScalarTower — Mathlib

English

If S, T act on R and IsScalarTower S T R holds, then the induced action on ℍ(R) also forms a scalar tower: IsScalarTower S T ℍ(R).

Русский

Если выполнено условие IsScalarTower для S, T над R, то и над ℍ(R) соблюдается IsScalarTower: IsScalarTower S T ℍ(R).

LaTeX

$$$$ \text{IsScalarTower } S T \mathbb{H}(R). $$$$

Lean4

instance [SMul S T] [SMul S R] [SMul T R] [IsScalarTower S T R] : IsScalarTower S T ℍ[R] :=
  inferInstanceAs <| IsScalarTower S T ℍ[R,-1,0,-1]

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