isScalarTower'' — Mathlib

English

If a tower of scalars exists for R,M,N, then there is a corresponding IsScalarTower R M (ULift N).

Русский

Если существует башня скаляров R → M → N, то существует IsScalarTower R M (ULift N).

LaTeX

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

Lean4

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

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