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