Determinant_of_Matrix_Product
Proveddeterminantlinear-algebramatrixproductproofwiki
Let and be a square matrices of order . Let be the determinant of . Let be the (conventional) matrix product of and . Then That is, the determinant of the product is equal to the product of the determinants.
Preamble
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Formal statement
theorem Determinant_of_Matrix_Product {R : Type _} [CommRing R] {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) : (A * B).det = A.det * B.det := by sorrySource