vec_eq_uncurry — Mathlib

English

For any matrix A, vec(A) equals the uncurry of the two-variable function i ↦ j ↦ A_{j i}. In words, vec encodes the entries of A by listing A_{ji} for all i,j.

Русский

Для любой матрицы A векторизация равна развёрнутой функцией двух переменных, где компонентами являются A_{j i}.

LaTeX

$$$$\operatorname{vec}(A) = \operatorname{Function.uncurry}(\lambda i\, j.\, A_{j i})$$$$

Lean4

theorem vec_eq_uncurry (A : Matrix m n R) : vec A = Function.uncurry fun i j => A j i :=
  rfl

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