single_mul_left_apply — Mathlib

English

For any indices i,j, any a ∈ α_i, and any family f, the j-th coordinate of single i (a · f(i)) equals (single i a) at j times f(j): (single i (a · f(i)))_j = (single i a)_j · f(j).

Русский

Для любых i,j, элемента a ∈ α_i и функции f, j-я координата единичной вставки i, умноженной на a и на f(i), равна произведению координаты a в i на j-ю координату f: (single i (a · f(i)))_j = (single i a)_j · f(j).

LaTeX

$$$\forall i,j:\quad (\operatorname{single}_i(a\cdot f(i)))_j = (\operatorname{single}_i a)_j \cdot f(j).$$$

Lean4

theorem single_mul_left_apply (i j : ι) (a : α i) (f : ∀ i, α i) : single i (a * f i) j = single i a j * f j :=
  (apply_single (fun i ↦ (· * f i)) (fun _ ↦ zero_mul _) _ _ _).symm

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