# Vectorization of matrices #

This file defines `Matrix.vec A`, the vectorization of a matrix `A`, formed by stacking the columns of A into a single large column vector.

Since mathlib indices matrices by arbitrary types rather than `Fin n`, the result of `Matrix.vec` on `A : Matrix m n R` is indexed by `n × m`. The `Fin (n * m)` interpretation can be restored by composing with `finProdFinEquiv.symm`:

    -- ![1, 2, 3, 4]
    #eval vec !![1, 3; 2, 4] ∘ finProdFinEquiv.symm

While it may seem more natural to index by `m × n`, keeping the indices in the same order, this would amount to stacking the rows into one long row, and goes against the literature. If you want this function, you can write `Matrix.vec Aᵀ` instead.

### References #

- Wikipedia

source
def Matrix.vec {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R) :
n × m → R

All the matrix entries, arranged into one column.

Equations

- A.vec ij = A ij.2 ij.1

Instances For

source
@[simp]
theorem Matrix.vec_of {m : Type u_2} {n : Type u_1} {R : Type u_3} (f : m → n → R) :
(of f).vec = Function.uncurry (flip f)
source
theorem Matrix.vec_transpose {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R) :
A.transpose.vec = A.vec ∘ Prod.swap
source
theorem Matrix.vec_eq_uncurry {m : Type u_1} {n : Type u_2} {R : Type u_3} (A : Matrix m n R) :
A.vec = Function.uncurry fun (i : n) (j : m) => A j i
source
theorem Matrix.vec_inj {m : Type u_1} {n : Type u_2} {R : Type u_3} {A B : Matrix m n R} :
A.vec = B.vec ↔ A = B
source
theorem Matrix.vec_bijective {m : Type u_3} {n : Type u_2} {R : Type u_1} :
Function.Bijective vec
source
theorem Matrix.vec_map {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} (A : Matrix m n R) (f : R → S) :
(A.map f).vec = f ∘ A.vec
source
@[simp]
theorem Matrix.vec_zero {m : Type u_3} {n : Type u_2} {R : Type u_1} [Zero R] :
vec 0 = 0
source
@[simp]
theorem Matrix.vec_eq_zero_iff {m : Type u_2} {n : Type u_3} {R : Type u_1} [Zero R] {A : Matrix m n R} :
A.vec = 0 ↔ A = 0
source
@[simp]
theorem Matrix.vec_add {m : Type u_2} {n : Type u_3} {R : Type u_1} [Add R] (A B : Matrix m n R) :
(A + B).vec = A.vec + B.vec
source
theorem Matrix.vec_neg {m : Type u_2} {n : Type u_3} {R : Type u_1} [Neg R] (A : Matrix m n R) :
(-A).vec = -A.vec
source
@[simp]
theorem Matrix.vec_sub {m : Type u_2} {n : Type u_3} {R : Type u_1} [Sub R] (A B : Matrix m n R) :
(A - B).vec = A.vec - B.vec
source
@[simp]
theorem Matrix.vec_smul {m : Type u_3} {n : Type u_4} {R : Type u_2} {α : Type u_1} [SMul α R] (r : α) (A : Matrix m n R) :
(r • A).vec = r • A.vec
source
theorem Matrix.vec_sum {ι : Type u_2} {m : Type u_3} {n : Type u_4} {R : Type u_1} [AddCommMonoid R] (s : Finset ι) (A : ι → Matrix m n R) :
(∑ i ∈ s, A i).vec = ∑ i ∈ s, (A i).vec
source
theorem Matrix.vec_dotProduct_vec {m : Type u_2} {n : Type u_3} {R : Type u_1} [AddCommMonoid R] [Mul R] [Fintype m] [Fintype n] (A B : Matrix m n R) :
A.vec ⬝ᵥ B.vec = (A.transpose * B).trace
source
theorem Matrix.star_vec {m : Type u_2} {n : Type u_3} {R : Type u_1} [Star R] (x : Matrix m n R) :
star x.vec = (x.map star).vec
source
theorem Matrix.star_vec_dotProduct_vec {m : Type u_2} {n : Type u_3} {R : Type u_1} [AddCommMonoid R] [Mul R] [Star R] [Fintype m] [Fintype n] (A B : Matrix m n R) :
star A.vec ⬝ᵥ B.vec = (A.conjTranspose * B).trace
source
theorem Matrix.vec_hadamard {m : Type u_2} {n : Type u_3} {R : Type u_1} [Mul R] (A B : Matrix m n R) :
(A.hadamard B).vec = A.vec * B.vec
source
@[simp]
theorem Matrix.vec_single {m : Type u_1} {n : Type u_2} {R : Type u_3} [DecidableEq m] [DecidableEq n] [Zero R] (i : m) (j : n) (r : R) :
(single i j r).vec = Pi.single (j, i) r
source
theorem Matrix.kronecker_mulVec_vec_of_commute {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [NonUnitalSemiring R] [Fintype m] [Fintype n] (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R) (hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)) :
(kroneckerMap (fun (x1 x2 : R) => x1 * x2) B A).mulVec X.vec = (A * X * B.transpose).vec

Technical lemma shared with `kronecker_mulVec_vec` and `vec_mul_eq_mulVec`.

source
theorem Matrix.vec_vecMul_kronecker_of_commute {l : Type u_2} {m : Type u_1} {n : Type u_4} {p : Type u_5} {R : Type u_3} [NonUnitalSemiring R] [Fintype m] [Fintype n] (A : Matrix m l R) (X : Matrix m n R) (B : Matrix n p R) (hA : ∀ (x : R) (i : m) (j : l), Commute (A i j) x) :
vecMul X.vec (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B A) = (A.transpose * X * B).vec

Technical lemma shared with `vec_vecMul_kronecker` and `vec_mul_eq_vecMul`.

source
theorem Matrix.kronecker_mulVec_vec {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [NonUnitalCommSemiring R] [Fintype m] [Fintype n] (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R) :
(kroneckerMap (fun (x1 x2 : R) => x1 * x2) B A).mulVec X.vec = (A * X * B.transpose).vec
source
theorem Matrix.vec_vecMul_kronecker {l : Type u_2} {m : Type u_1} {n : Type u_4} {p : Type u_5} {R : Type u_3} [NonUnitalCommSemiring R] [Fintype m] [Fintype n] (A : Matrix m l R) (X : Matrix m n R) (B : Matrix n p R) :
vecMul X.vec (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B A) = (A.transpose * X * B).vec
source
theorem Matrix.vec_mul_eq_mulVec {l : Type u_2} {m : Type u_3} {n : Type u_1} {R : Type u_4} [Semiring R] [Fintype m] [Fintype n] [DecidableEq n] (A : Matrix l m R) (B : Matrix m n R) :
(A * B).vec = (kroneckerMap (fun (x1 x2 : R) => x1 * x2) 1 A).mulVec B.vec
source
theorem Matrix.vec_mul_eq_vecMul {m : Type u_1} {n : Type u_2} {p : Type u_4} {R : Type u_3} [Semiring R] [Fintype m] [Fintype n] [DecidableEq m] (A : Matrix m n R) (B : Matrix n p R) :
(A * B).vec = vecMul A.vec (kroneckerMap (fun (x1 x2 : R) => x1 * x2) B 1)