single_mul — Mathlib

English

For any a and b1,b2 in β with MulZeroClass structure, single a (b1 * b2) = single a b1 * single a b2.

Русский

Для любых a и b1,b2 в β выполняется single a (b1 * b2) = single a b1 * single a b2.

LaTeX

$$$\\mathrm{single}(a, b_1 b_2) = \\mathrm{single}(a, b_1) \\cdot \\mathrm{single}(a, b_2)$$$

Lean4

@[simp]
theorem single_mul (a : α) (b₁ b₂ : β) : single a (b₁ * b₂) = single a b₁ * single a b₂ :=
  (zipWith_single_single _ _ _ _ _).symm

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