English
Let β be a multiplicative structure (a semigroup or monoid) and let α act on β via a scalar action that commutes with β-multiplication. Then for all s in α and x, y in β, we have x * (s • y) = s • (x * y).
Русский
Пусть β имеет умножение и задано скалярное действие α на β, совместимое с умножением в β. Тогда для всех s ∈ α и x, y ∈ β выполняется x · (s • y) = s • (x · y).
LaTeX
$$$\\\\forall s \\\\in \\\\alpha, \\\\forall x, y \\\\in \\\\beta, \\\\ x \\\\cdot (s \\\\cdot y) = s \\\\cdot (x \\\\cdot y).$$$
Lean4
/-- Note that the `SMulCommClass α β β` typeclass argument is usually satisfied by `Algebra α β`. -/
@[to_additive]
theorem mul_smul_comm [Mul β] [SMul α β] [SMulCommClass α β β] (s : α) (x y : β) : x * s • y = s • (x * y) :=
(smul_comm s x y).symm
