English
Distributivity of smul over multiplication: a • (b1 * b2) = a • b1 * a • b2 for a ∈ M, b1,b2 ∈ N under MulDistribMulAction.
Русский
Дистрибутивность смула над умножением: a • (b1 * b2) = a • b1 * a • b2 для a ∈ M, b1,b2 ∈ N при MulDistribMulAction.
LaTeX
$$$ a \cdot (b_1 b_2) = a \cdot b_1 \; a \cdot b_2 $$$
Lean4
theorem smul_mul' (a : M) (b₁ b₂ : N) : a • (b₁ * b₂) = a • b₁ * a • b₂ :=
MulDistribMulAction.smul_mul ..