isScalarTower' — Mathlib

English

Under SMul structures and IsScalarTower assumptions, ULift inherits a scalar tower: IsScalarTower R (ULift M) N.

Русский

При наличии структур SMul и IsScalarTower ULift наследует башню скаляров: IsScalarTower R (ULift M) N.

LaTeX

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

Lean4

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

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