Transpose_of_Matrix_Product_v2
Provedlinear-algebramatrixproofwikitranspose
Let and be matrices over a commutative ring such that is defined. Then is defined, and where is the transpose of .
Preamble
import Mathlib.Data.Matrix.Basic
Formal statement
theorem Transpose_of_Matrix_Product_v2 {R : Type _} [CommRing R] {l m n : ℕ} (A : Matrix (Fin l) (Fin m) R) (B : Matrix (Fin m) (Fin n) R) : Matrix.transpose (A * B) = Matrix.transpose B * Matrix.transpose A := by sorrySource