Classic mathematics

Cayley–Hamilton in 2 × 2

A matrix satisfies its own characteristic polynomial. Unpack that statement into four scalar identities.

-- Top 100 #49: Cayley–Hamilton in 2 × 2
-- History: 1858 · Cayley.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: The characteristic polynomial of a 2×2 matrix uses only its trace and determinant.
-- Scope: Proves all four entries of A² − trace(A)A + det(A)I = 0 for arbitrary integer 2×2 matrices.
-- Source: https://lurch.plus/100/

-- A = [a b; c d], trace = a+d, determinant = a*d-b*c.
theorem cayley_hamilton_2 (a b c d : Int) :
    (a*a+b*c) - (a+d)*a + (a*d-b*c) = 0 ∧
    (a*b+b*d) - (a+d)*b = 0 ∧
    (c*a+d*c) - (a+d)*c = 0 ∧
    (c*b+d*d) - (a+d)*d + (a*d-b*c) = 0 := by
  constructor
  · grind
  constructor
  · grind
  constructor <;> grind

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`grind`

Combines logical reasoning and polynomial normalization to construct a proof term that Lean checks.

`Int`

Exact integers, including negatives. Unlike Nat subtraction, integer subtraction does not truncate at zero.

Background and proof scope

1858 · Cayley

The characteristic polynomial of a 2×2 matrix uses only its trace and determinant.

Proves all four entries of A² − trace(A)A + det(A)I = 0 for arbitrary integer 2×2 matrices.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Use a=1, b=2, c=3, d=4 to compute the trace and determinant by hand.