vec_single — Mathlib

English

The vectorization of a matrix unit matrix is the corresponding Pi.single basis vector: vec(Matrix.single i j r) = Pi.single (j,i) r.

Русский

Векторизация единичной матрицы даёт соответствующий базисный вектор: vec(single i j r) = Pi.single (j,i) r.

LaTeX

$$$$\operatorname{vec}(\mathrm{single}(i,j,r)) = \mathrm{Pi.single}( (j,i) )\, r$$$$

Lean4

@[simp]
theorem vec_single [DecidableEq m] [DecidableEq n] [Zero R] (i : m) (j : n) (r : R) :
    vec (Matrix.single i j r) = Pi.single (j, i) r :=
  by
  rw [single_eq_of_single_single, vec_of, Function.uncurry_flip, Pi.uncurry_single_single]
  exact Pi.single_comp_equiv (Equiv.prodComm _ _) _ _

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