isScalarTower' — Mathlib

English

A variant of IsScalarTower for Set β → Set γ, ensuring the associativity of scalar action holds in the Set-level construction via image-left commutation.

Русский

Вариант IsScalarTower для Set β → Set γ обеспечивает ассоциативность скалярного действия в конструировании множества через изображение слева.

LaTeX

$$$ IsScalarTower α (Set β) (Set γ) \Rightarrow smul_assoc'_proof: \forall a,b,T, image2_image_left_comm (smul_assoc a b T).$$$

Lean4

@[to_additive]
instance isScalarTower' [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α (Set β) (Set γ) :=
  ⟨fun _ _ _ ↦ image2_image_left_comm <| smul_assoc _⟩

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