English
For any matrix A, transposeᵣ A equals transpose A.
Русский
Для любой матрицы A транспонирование, определённое как transposeᵣ, совпадает с обычным транспонированием.
LaTeX
$$$\\forall A, \\; A^{\\text{transpose}^\\!_r} = A^{\\top}$$$
Lean4
/-- This can be used to prove
```lean
example (a b c d : α) : transpose !![a, b; c, d] = !![a, c; b, d] := (transposeᵣ_eq _).symm
```
-/
@[simp]
theorem transposeᵣ_eq : ∀ {m n} (A : Matrix (Fin m) (Fin n) α), transposeᵣ A = transpose A
| _, 0, _ => Subsingleton.elim _ _
| m, n + 1, A =>
Matrix.ext fun i j => by
simp_rw [transposeᵣ, transposeᵣ_eq]
refine i.cases ?_ fun i => ?_
· dsimp
rw [FinVec.map_eq, Function.comp_apply]
· simp only [of_apply, Matrix.cons_val_succ]
rfl
