Classic mathematics

Cramer’s rule in 2 × 2

Derive the numerators in the formula for solving two simultaneous linear equations.

-- Top 100 #97: Cramer’s rule in 2 × 2
-- History: 1750 · Cramer.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Eliminating y and eliminating x produces the two determinant numerators.
-- Scope: Proves the division-free equations det(A)x=ed−bf and det(A)y=af−ec for any integer solution. Division and existence of a solution are not asserted.
-- Source: https://lurch.plus/100/

theorem cramer_numerators (a b c d e f x y : Int)
    (first : a*x+b*y = e) (second : c*x+d*y = f) :
    (a*d-b*c)*x = e*d-b*f ∧
    (a*d-b*c)*y = a*f-e*c := by
  constructor <;> grind

-- 2x+y=5 and x-y=1 have the solution x=2, y=1.
example : 2*(2 : Int)+1=5 ∧ 2-1=1 := by decide

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

1750 · Cramer

Eliminating y and eliminating x produces the two determinant numerators.

Proves the division-free equations det(A)x=ed−bf and det(A)y=af−ec for any integer solution. Division and existence of a solution are not asserted.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

File checked successfully.

Exercise

Why must the determinant be nonzero before dividing to solve for x and y?