Linear Algebra

Cayley–Hamilton Theorem

Every square matrix satisfies its own characteristic polynomial

lean4-prooflinear-algebravisualization

Spectral Theorem

Every real symmetric matrix is orthogonally diagonalizable

lean4-prooflinear-algebravisualization

Rank–Nullity Theorem

The dimensions of image and kernel of a linear map sum to the domain dimension

lean4-prooflinear-algebravisualization

Determinant Multiplicativity

The determinant of a product equals the product of determinants

lean4-prooflinear-algebravisualization

Cramer's Rule

Explicit determinant formula for the solution of a linear system

lean4-prooflinear-algebravisualization

Lagrange Interpolation

Given n distinct nodes, there is a unique polynomial of degree < n passing through all n points.

lean4-prooflinear-algebravisualization

Newton's Identities

Power sums and elementary symmetric polynomials satisfy a mutual recursion that lets each determine the other.

lean4-prooflinear-algebravisualization

LU Decomposition

Every invertible matrix factors as a unit-lower-triangular matrix times an upper-triangular matrix.

lean4-prooflinear-algebravisualization

QR Decomposition

Every invertible real matrix factors as a product of an orthogonal matrix and an upper-triangular matrix.

lean4-prooflinear-algebravisualization

Singular Value Decomposition

Every real matrix factors as U times a diagonal matrix of singular values times V-transpose.

lean4-prooflinear-algebravisualization

Gram–Schmidt Orthogonalization

Any linearly independent sequence can be transformed into an orthogonal sequence spanning the same subspace.

lean4-prooflinear-algebravisualization

Hadamard's Inequality

The absolute value of a determinant is at most the product of the Euclidean norms of its columns.

lean4-prooflinear-algebravisualization

Cauchy–Binet Formula

The determinant of a product AB equals the sum over all maximal minors of A times the corresponding minors of B.

lean4-prooflinear-algebravisualization

Jordan Canonical Form

Every square matrix over an algebraically closed field is similar to a direct sum of Jordan blocks.

lean4-prooflinear-algebravisualization

Schur Decomposition

Every square complex matrix is unitarily similar to an upper triangular matrix.

lean4-prooflinear-algebravisualization

Polar Decomposition

Every invertible matrix factors as a unitary times a positive definite matrix.

lean4-prooflinear-algebravisualization

Sylvester Determinant Theorem

det(Im + AB) = det(In + BA) for any m×n matrix A and n×m matrix B.

lean4-prooflinear-algebravisualization

Trace Cyclic Property

The trace of a product of matrices is invariant under cyclic permutations: tr(AB) = tr(BA).

lean4-prooflinear-algebravisualization

Minimal Polynomial

The minimal polynomial of a matrix is the monic polynomial of least degree that annihilates it.

lean4-prooflinear-algebravisualization

Diagonalizability Criterion

A matrix is diagonalizable if and only if its minimal polynomial is squarefree.

lean4-prooflinear-algebravisualization

Companion Matrix

The companion matrix of a monic polynomial has that polynomial as its characteristic polynomial.

lean4-prooflinear-algebravisualization