English
Under suitable assumptions, the product of scalars acts distributively over products: (a • b) * (c • d) = (a * c) • (b * d).
Русский
При надлежащих предположениях произведение скаляров действует распределительно на произведения: (a • b) * (c • d) = (a * c) • (b * d).
LaTeX
$$$\\\\forall a \\\\in \\\\alpha, b \\\\in \\\\beta, c \\\\in \\\\alpha, 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 smul_mul_smul_comm [Mul α] [Mul β] [SMul α β] [IsScalarTower α β β] [IsScalarTower α α β] [SMulCommClass α β β]
(a : α) (b : β) (c : α) (d : β) : (a • b) * (c • d) = (a * c) • (b * d) := by
have : SMulCommClass β α β := .symm ..; exact smul_smul_smul_comm a b c d
