smul_mul' — Mathlib

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 ..

Похожие утверждения