single_mul_right_apply — Mathlib

English

For all i,j, f, a ∈ α_i, the j-th coordinate of single i (f(i) · a) equals f(j) times the j-th coordinate of single i a: single i (f i · a) j = f j · single i a j.

Русский

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

LaTeX

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

Lean4

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

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