single_mul_left — Mathlib

English

For a fixed index i and elements a ∈ α_i and f ∈ ∀ i, α_i, the function single i (a · f(i)) equals the product of single i a with f, i.e., single i (a · f(i)) = single i a · f.

Русский

Для фиксированного индекса i и элементов a ∈ α_i, f ∈ ∀ i α_i выполняется: единичная вставка i произведения a с f(i) равна произведению единичной вставки i a на f.

LaTeX

$$$\forall a:\; \operatorname{single}_i(a\cdot f(i)) = \operatorname{single}_i a \cdot f.$$$

Lean4

theorem single_mul_left (a : α i) : single i (a * f i) = single i a * f :=
  funext fun _ ↦ single_mul_left_apply _ _ _ _

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