transposeᵣ — Mathlib

English

The transposition built via Fin-indexing agrees with the standard matrix transpose; i.e., transposeᵣ A = transpose A for all A.

Русский

Построение транспонирования с помощью индексов Fin совпадает с обычным транспонированием матрицы.

LaTeX

$$$\\text{transpose}^{\\!\\!\\!\\!}_{\\mathsf{r}} A = \\text{transpose } A$$$

Lean4

/-- `Matrix.transpose` with better defeq for `Fin` -/
def transposeᵣ : ∀ {m n}, Matrix (Fin m) (Fin n) α → Matrix (Fin n) (Fin m) α
  | _, 0, _ => of ![]
  | _, _ + 1, A => of <| vecCons (FinVec.map (fun v : Fin _ → α => v 0) A) (transposeᵣ (A.submatrix id Fin.succ))

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