English
If α acts on β and β multiplies, then (a*b) • (c*d) = (a • c) * (b • d) for a,b ∈ α and c,d ∈ β.
Русский
Если α действует на β и β умножается, то (a*b) • (c*d) = (a•c) * (b•d) для a,b ∈ α и c,d ∈ β.
LaTeX
$$$\\\\forall a,b \\\\in \\\\alpha, c,d \\\\in \\\\beta, \\\\ (a \\\\cdot b) \\\\cdot (c \\\\cdot d) = (a \\\\cdot c) \\\\cdot (b \\\\cdot d).$$$
Lean4
/-- Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually
satisfied by `Algebra α β`. -/
@[to_additive]
theorem mul_smul_mul_comm [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] [IsScalarTower α α β] [SMulCommClass α β β]
(a b : α) (c d : β) : (a * b) • (c * d) = (a • c) * (b • d) :=
smul_smul_smul_comm a b c d
