English
If multiple scalar actions form towers, then the base level action is also a tower.
Русский
Если последовательности действия по нескольким шарикам образуют башни, то базовый уровень образует башню.
LaTeX
$$$\\text{IsScalarTower } M N Q \\Rightarrow \\text{IsScalarTower } M N Q$$$
Lean4
/-- Let `Q / P / N / M` be a tower. If `Q / N / M`, `Q / P / M` and `Q / P / N` are
scalar towers, then `P / N / M` is also a scalar tower.
-/
@[to_additive]
theorem to₁₂₃ (M N P Q) [SMul M N] [SMul M P] [SMul M Q] [SMul N P] [SMul N Q] [SMul P Q] [FaithfulSMul P Q]
[IsScalarTower M N Q] [IsScalarTower M P Q] [IsScalarTower N P Q] : IsScalarTower M N P where
smul_assoc m n p := by simp_rw [← (smul_left_injective' (α := Q)).eq_iff, smul_assoc]
