Properties of determinants in Isabelle

I would like to use the facts that $$\det AB=\det A \det B$$ and $$\det A = \det A^t$$ to prove that $$\det AA^t = (\det A)^2$$ in Isabelle. Is there a fast way to do this without doing this from scratch?

You don't have to do this from scratch. The facts in HOL-Analysis.Determinants and related theories suffice.

Your first fact, $$\det AB=\det A \det B$$, is proposition Determinants.det_mul, which reads det (?A ** ?B) = det ?A * det ?B.

Your second fact, $$\det A = \det A^t$$, is called Determinants.det_transpose, reading det (Finite_Cartesian_Product.transpose ?A) = det ?A.

Mixing in some detail on the formulation of powers, one gets:

theory Scratch
imports "HOL-Analysis.Determinants"
begin

lemma
shows ‹det (A ** transpose A) = det A ^ 2›
using det_mul det_transpose
unfolding power2_eq_square
by metis


sledgehammer has also told me that the simplifier is almost ready to prove your goal directly. It proposed the following proof:

lemma
shows ‹det (A ** transpose A) = det A ^ 2›

• @CraigFeinstein: ** is the syntax for matrix_matrix_mult, not for Cartesian products. But it's part of the scope/theory called HOL-Analysis.Finite_Cartesian_Product. All basic matrix defs can be found there. The background is that vectors are understood through finite (Cartesian) product types. A specific $n$-dimensional vector over say $\mathbb R$ is a member of the Cartesian $n$-product $\mathbb R \times \mathbb R \times \ldots \times \mathbb R$. Matrices are vectors of vectors. Commented Jul 16 at 9:22