cons_transpose — Mathlib

English

Transposing the matrix formed by vecCons v A yields a matrix whose i-th row is vecCons (v i) (A^T i).

Русский

Транспонирование матрицы вида vecCons v A даёт матрицу, у которой i-я строка равна vecCons (v i) (A^T i).

LaTeX

$$$(\\mathrm{of}(\\mathrm{vecCons}\\, v\\, A))^T = \\mathrm{of}\\, (\\lambda i \\mapsto \\mathrm{vecCons}(v i) (A^T i))$$$

Lean4

@[simp]
theorem cons_transpose (v : n' → α) (A : Matrix (Fin m) n' α) :
    (of (vecCons v A))ᵀ = of fun i => vecCons (v i) (Aᵀ i) :=
  by
  ext i j
  refine Fin.cases ?_ ?_ j <;> simp

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