English
With appropriate scalar towers and SMulCommClass, the action distributes over nested smuls: (a • b) • c • d = (a • c) • b • d for a ∈ α, b ∈ β, c ∈ γ, d ∈ δ.
Русский
При наличии требуемых торов скаляров и SMulCommClass выполняется распределение по вложенным смулам: (a • b) • c • d = (a • c) • b • d.
LaTeX
$$$\\\\forall a \\\\in \\\\alpha, b \\\\in \\\\beta, c \\\\in \\\\gamma, d \\\\in \\\\delta,\\\\ (a \\\\cdot b) \\\\cdot c \\\\cdot d = (a \\\\cdot c) \\\\cdot b \\\\cdot d.$$$
Lean4
@[to_additive]
theorem smul_smul_smul_comm [SMul α β] [SMul α γ] [SMul β δ] [SMul α δ] [SMul γ δ] [IsScalarTower α β δ]
[IsScalarTower α γ δ] [SMulCommClass β γ δ] (a : α) (b : β) (c : γ) (d : δ) : (a • b) • c • d = (a • c) • b • d :=
by rw [smul_assoc, smul_assoc, smul_comm b]
