19.2. Proving irreducibility🔗

The bare tactic closes an Irreducible goal:

open Polynomial

example : Irreducible (X ^ 2 - 2 : Polynomial ℤ) := by⊢ Irreducible (X ^ 2 - 2)
  irreducibilityAll goals completed! 🐙

It can also be used as a term:

open Polynomial

theorem sqrt2_irred :
    Irreducible (X ^ 2 - 2 : Polynomial ℤ) :=
  irreducibility (X ^ 2 - 2 : Polynomial ℤ)

With an explicit polynomial in tactic mode, the unnamed form adds a hypothesis called this, while the named form chooses a name:

open Polynomial

example :
    Irreducible (X ^ 2 - 2 : Polynomial ℤ) ∧
      Irreducible (X ^ 2 + X + 1 : Polynomial ℤ) := by⊢ Irreducible (X ^ 2 - 2) ∧ Irreducible (X ^ 2 + X + 1)
  irreducibility (X ^ 2 - 2 : Polynomial ℤ)this:Irreducible (X ^ 2 - 2)⊢ Irreducible (X ^ 2 - 2) ∧ Irreducible (X ^ 2 + X + 1)
  irreducibility h : (X ^ 2 + X + 1 : Polynomial ℤ)this:Irreducible (X ^ 2 - 2)h:Irreducible (X ^ 2 + X + 1)⊢ Irreducible (X ^ 2 - 2) ∧ Irreducible (X ^ 2 + X + 1)
  exact ⟨this, h⟩All goals completed! 🐙

The same syntax proves the Mathlib-free predicate on dense integer polynomials:

open Hex

def quadZ : ZPoly := #p[1, 0, 1]

theorem quadZ_irred : ZPoly.Irreducible quadZ :=
  irreducibility quadZ

The correspondence library proves that Hex.ZPoly.Irreducible agrees with Mathlib's Irreducible predicate after conversion to Polynomial ℤ.