Determinant of Matrix Exponential is Non-Zero

Theorem

Let $\mathbf A$ be a square matrix.

Let $t \in \R$ be a real number.

Let $e^{\mathbf A t}$ denote the matrix exponential of $\mathbf A$.

Then:

$\det e^{\mathbf A t} \ne 0$

where $\det$ denotes the determinant.

Proof

This theorem requires a proof. In particular: The below outlines an approach. Details need to be completed. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by crafting such a proof. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{ProofWanted}} from the code. If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.

The linear system $x' = \mathbf A x$ has $n$ linearly independent solutions.

Putting together these solutions as columns in a matrix creates a matrix solution to the differential equation, considering the initial conditions for the matrix exponential.

From Existence and Uniqueness Theorem for 1st Order IVPs, this solution is unique.

By linear independence of its columns:

$\det e^{\mathbf A t} \ne 0$

This page has been identified as a candidate for refactoring of basic complexity. In particular: The following is a separate proof and would need to be added to another transcluded page. Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

The nonzero determinant property also follows as a corollary to Liouville's Theorem (Differential Equations).