Classic mathematics

The factor & remainder identity

Express the factor theorem directly, without importing a polynomial library.

-- Top 100 #89: The factor & remainder identity
-- History: First discovery date unknown.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Subtracting p(r) from p(x) makes x−r appear as a factor.
-- Scope: Proves the remainder identity for an arbitrary integer quadratic and derives factorization when r is a root. Arbitrary-degree polynomials are not modeled.
-- Source: https://lurch.plus/100/

def polynomial (a b c x : Int) := a*x^2+b*x+c

theorem remainder_identity (a b c x r : Int) :
    polynomial a b c x - polynomial a b c r =
      (x-r)*(a*(x+r)+b) := by
  unfold polynomial
  grind

theorem root_factor (a b c x r : Int)
    (root : polynomial a b c r = 0) :
    polynomial a b c x = (x-r)*(a*(x+r)+b) := by
  have h := remainder_identity a b c x r
  omega

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

First discovery date unknown

Subtracting p(r) from p(x) makes x−r appear as a factor.

Proves the remainder identity for an arbitrary integer quadratic and derives factorization when r is a root. Arbitrary-degree polynomials are not modeled.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

File checked successfully.

Exercise

Use the identity for x²−5x+6 at r=2. What is the remaining factor?