English
Let M N P Q be actions forming towers M→N→P, M→N→Q and N→P→Q; then M→P→Q is a scalar tower.
Русский
Пусть M,N,P,Q образуют башни действий; тогда M→P→Q образует скалярную башню.
LaTeX
$$$ \text{IsScalarTower } M P Q$$$
Lean4
/-- Let `Q / P / N / M` be a tower. If `P / N / M`, `Q / N / M` and `Q / P / N` are
scalar towers, then `Q / P / M` is also a scalar tower.
-/
@[to_additive]
theorem to₁₃₄ (M N P Q) [SMul M N] [SMul M P] [SMul M Q] [SMul P Q] [Monoid N] [MulAction N P] [MulAction N Q]
[IsScalarTower M N P] [IsScalarTower M N Q] [IsScalarTower N P Q] : IsScalarTower M P Q where
smul_assoc m p q := by rw [← smul_one_smul N m, smul_assoc, smul_one_smul]
