Eigenvalues of a $2\times2$ matrix from its trace and determinant

Proved

Matrix.charpoly_roots_fin_two_of_trace_det

by Mazecto · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebra

Let $R$ be an integral domain, $V$ a $2\times2$ matrix over $R$ and $\mu_1,\mu_2\in R$ with $\operatorname{tr}V=\mu_1+\mu_2$ and $\det V=\mu_1\mu_2$ . Then the multiset of roots of the characteristic polynomial of $V$ is $\{\mu_1,\mu_2\}$ , i.e. $\chi_V(X)=(X-\mu_1)(X-\mu_2)$ .

Preamble

import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
import Mathlib.Algebra.Polynomial.Roots

open Polynomial

Formal statement

theorem Matrix.charpoly_roots_fin_two_of_trace_det {R : Type*} [CommRing R] [IsDomain R] {V : Matrix (Fin 2) (Fin 2) R} {μ₁ μ₂ : R}
    (htr : V.trace = μ₁ + μ₂) (hdet : V.det = μ₁ * μ₂) :
    V.charpoly.roots = {μ₁, μ₂} := by sorry

Source

Standard linear algebra (Vieta's formulas for the characteristic polynomial

X^2-\operatorname{tr}V\,X+\det V

of a

2\times2

matrix).

View graph

Eigenvalues of a 2×22\times22×2 matrix from its trace and determinant

Eigenvalues of a $2\times2$ matrix from its trace and determinant