English
If you have scalar actions of α on β and α on γ, and β on γ, forming a scalar tower, then the pointwise action on Set γ inherits a consistent IsScalarTower structure: (α, Set β, Set γ).
Русский
При наличии действий скаляров на β и γ и согласованной пирамиды усилий α → β → γ, множество Set γ наследует корректную структуру IsScalarTower.
LaTeX
$$$\text{IsScalarTower } α β γ \Rightarrow IsScalarTower α (Set β) (Set γ)$ with smul_assoc given by image commutativity: smul_assoc a b T = image2_image_left_comm (smul_assoc a b T).$$
Lean4
@[to_additive]
instance isScalarTower [SMul α β] [SMul α γ] [SMul β γ] [IsScalarTower α β γ] : IsScalarTower α β (Set γ) where
smul_assoc a b T := by simp only [← image_smul, image_image, smul_assoc]
