isScalarTower — Mathlib

English

If SMul R M, SMul M N, SMul R N and IsScalarTower R M N hold, then ULift R defines IsScalarTower (ULift R) M N; scalar actions commute with ULift.

Русский

Если есть действия скаляров R на M и N и IsScalarTower R M N, то ULift R сохраняет это отношение для ULift M и N: действует тождественные тензоры.

LaTeX

$$$IsScalarTower (ULift R) M N$$$

Lean4

instance isScalarTower [SMul R M] [SMul M N] [SMul R N] [IsScalarTower R M N] : IsScalarTower (ULift R) M N :=
  ⟨fun x y z => show (x.down • y) • z = x.down • y • z from smul_assoc _ _ _⟩

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