English
If there exists a surjective map h: M → N given by m ↦ m • (1 : N), then N → P → Q forms a scalar tower.
Русский
Если существует сюрьективное отображение h: M → N, заданное h(m) = m • 1, то N → P → Q образует скалярную башню.
LaTeX
$$$ \text{IsScalarTower } N P Q$$$
Lean4
/-- Let `Q / P / N / M` be a tower. If `P / N / M`, `Q / P / M` and `Q / P / N` are
scalar towers, then `Q / 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] [Monoid P] [MulAction P Q]
[IsScalarTower M N P] [IsScalarTower M P Q] [IsScalarTower N P Q] : IsScalarTower M N Q where
smul_assoc m n q := by rw [← smul_one_smul P, smul_assoc m, smul_assoc, smul_one_smul]
