Determinant_of_Transpose_v2
Proveddeterminantlinear-algebramatrixproofwikitranspose
Let be a square matrix of order . Let be the determinant of . Let be the transpose of . Then
Preamble
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Formal statement
theorem Determinant_of_Transpose_v2 {R : Type _} [CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) : (Matrix.transpose A).det = A.det := by sorrySource