Transpose_of_Transpose_of_Matrix_v2

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

linear-algebramatrixproofwikitranspose

Let $\mathbf A$ be a matrix. Let $\mathbf A^\intercal$ be the transpose of $\mathbf A$ . Then $\paren {\mathbf A^\intercal}^\intercal = \mathbf A$

Preamble

import Mathlib.Data.Matrix.Basic

Formal statement

theorem Transpose_of_Transpose_of_Matrix_v2 {R : Type _} [CommRing R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) : Matrix.transpose (Matrix.transpose A) = A := by sorry

Source

https://proofwiki.org/wiki/Transpose_of_Transpose_of_Matrix

View graph