How to use Rational Root Theorem?

Stream: new members

[Ilmārs Cīrulis]

Got this far for now. Is this good start?
(Polynomial taken from #mathlib4 > polynomials123 )

import Mathlib
open Polynomial

noncomputable def f: ℤ[X] := X^3 + C 3 * X^2 - C 8

theorem natDegree_of_f_is_three: f.natDegree = 3 := by rw [f]; compute_degree!

theorem leading_coef_of_f: f.leadingCoeff = 1 := by
  rw [leadingCoeff, natDegree_of_f_is_three, f]; simp

theorem aux (r: ℚ): f.aeval r ≠ 0 := by
  intro H
  have H0 := num_dvd_of_is_root H
  have H1 := den_dvd_of_is_root H
  rw [leading_coef_of_f] at H1
  unfold f at H0; simp at *
  have H2: ↑(IsFractionRing.den ℤ r) ∈ [(-1: ℤ), 1] := by sorry
  have H3: IsFractionRing.num ℤ r ∈ [-8, -4, -2, -1, 1, 2, 4, 8] := by sorry
  simp at H3 H2; obtain H3 | H3 | H3 | H3 | H3 | H3 | H3 | H3 := H3 <;> obtain H2 | H2 := H2
  . have Hr: r = (8: ℚ) := by
      have H4 := IsFractionRing.mk'_num_den' ℤ r
      rw [<- H4, H3, H2]; simp
    rw [Hr, f] at H; simp at H; rw [map_ofNat, map_ofNat] at H; norm_num at H
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry
  . sorry

[Aaron Liu]

Unfortunately one of your sorrys is not provable, because both 1 and -1 divide 1.

[Ilmārs Cīrulis]

Ok, that's fixable

[Ilmārs Cīrulis]

[Edited proof part in the original post.]

Now I have only to prove H2 and H3 (about integer divisors of 1 and 8) and (similarly to the first case) fill remaining 15 cases. Then aux theorem will be done.

[Ilmārs Cīrulis]

What's the best way to say (in Lean) that p: ℚ[X] has only integer coefficients?

[Ilmārs Cīrulis]

WIll go with
def all_coeffs_integer(p: ℚ[X]): Prop := ∀ (c: ℚ), c ∈ p.coeffs → c.den = 1

[Ilmārs Cīrulis]

Would such two theorems be useful?

import Mathlib
open Polynomial

def all_coeffs_integer (p: ℚ[X]): Prop := ∀ (c: ℚ), c ∈ p.coeffs → c.den = 1

theorem rational_root_theorem_den (p: ℚ[X]) (Hp: all_coeffs_integer p) (r: ℚ): r ∈ p.roots → r.den ∣ p.leadingCoeff.num.natAbs := by
  sorry

theorem rational_root_theorem_num (p: ℚ[X]) (Hp: all_coeffs_integer p) (r: ℚ): r ∈ p.roots → r.num ∣ (p.coeff 0).num := by
  sorry

[Ilmārs Cīrulis]

Current state (stuck in multiple ways :sob: ):

import Mathlib
open Polynomial

theorem aux (p: ℤ[X]) (n: ℕ):
    ((p.map (Int.castRingHom ℚ)).coeff n).den = 1 := by
  simp

theorem aux0 (r: ℚ): r.den = (IsFractionRing.den ℤ r: ℤ).natAbs := by
  sorry

theorem rational_root_theorem_den (p: ℤ[X]) (r: ℚ):
    r ∈ (p.map (Int.castRingHom ℚ)).roots → r.den ∣ p.leadingCoeff.natAbs := by
  simp; intro H H0
  have H1: p.aeval r = 0 := by
    sorry
  apply den_dvd_of_is_root at H1
  obtain ⟨d, H1⟩ := H1
  rw [aux0, H1]; simp

theorem rational_root_theorem_num (p: ℤ[X]) (r: ℚ):
    r ∈ (p.map (Int.castRingHom ℚ)).roots → r.num.natAbs ∣ (p.coeff 0).natAbs := by
  sorry

[Ruben Van de Velde]

You nerd-sniped me for the first one, but I'll leave the rest to you.

[Ruben Van de Velde]

import Mathlib
open Polynomial

theorem aux (p: ℤ[X]) (n: ℕ):
    ((p.map (Int.castRingHom ℚ)).coeff n).den = 1 := by
  simp
theorem aux2 (q : ℚ) (n: ℤ ) (d : ℕ) (hd : d ≠ 0) (red: IsCoprime n d) (h : q * d = n) : d = q.den ∧ n = q.num := by
  replace h : q = n / d := by rw [← h]; rw [mul_div_cancel_right₀]; simp_all
  subst h
  constructor
  · apply Nat.cast_injective (R := ℤ)
    convert (Rat.den_div_eq_of_coprime (a := n) (b := d) ?_ ?_).symm
    · simp_all [pos_iff_ne_zero]
    · rwa [← @Int.isCoprime_iff_nat_coprime]
  · convert (Rat.num_div_eq_of_coprime (a := n) (b := d) ?_ ?_).symm
    · simp_all [pos_iff_ne_zero]
    · rwa [← @Int.isCoprime_iff_nat_coprime]


theorem aux1 (r : ℚ) : (IsFractionRing.den ℤ r: ℤ).natAbs = r.den ∧ (IsFractionRing.num ℤ r: ℤ).natAbs = r.num.natAbs := by
  have h0 := IsFractionRing.mk'_num_den ℤ r
  rw [ IsLocalization.mk'_eq_iff_eq_mul, eq_comm] at h0
  simp at h0
  have := Int.natAbs_eq (IsFractionRing.den ℤ r: ℤ)
  cases this with
  | inl h =>
    have := aux2 r (IsFractionRing.num ℤ r) ((IsFractionRing.den ℤ r: ℤ).natAbs) ?_ ?_ ?_
    refine ⟨this.1, by rw [this.2]⟩
    · simp
    · have h1 := IsFractionRing.num_den_reduced ℤ r
      have := IsRelPrime.isCoprime h1
      simp
      exact (IsCoprime.abs_right_iff (IsFractionRing.num ℤ r) ↑(IsFractionRing.den ℤ r)).mpr this
    · convert h0
      apply_fun Int.cast (R := ℚ) at h
      convert h.symm
  | inr h =>
    rw [h] at h0
    simp only [Int.cast_neg, mul_neg] at h0
    rw [@neg_eq_iff_eq_neg] at h0
    have := aux2 _ _ _ ?_ ?_ h0
    refine ⟨by simpa using this.1, by rw [← this.2]; simp⟩
    · simp
    · have h1 := IsFractionRing.num_den_reduced ℤ r
      have := IsRelPrime.isCoprime h1
      simp [IsCoprime.neg_left_iff]
      exact (IsCoprime.abs_right_iff (IsFractionRing.num ℤ r) ↑(IsFractionRing.den ℤ r)).mpr this

theorem aux0 (r: ℚ): r.den = (IsFractionRing.den ℤ r: ℤ).natAbs := by
  exact (aux1 r).1.symm

[Ruben Van de Velde]

Actually, here's two as well

  have H1: p.aeval r = 0 := by
    rw [← @eval_map_algebraMap]
    simpa using H0

[Ilmārs Cīrulis]

Here is what I have done:

/-
Copyright (c) 2025 Ilmārs Cīrulis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ilmārs Cīrulis
-/
import Mathlib.Analysis.Normed.Field.Lemmas
import Mathlib.Data.Int.Star
import Mathlib.RingTheory.Polynomial.RationalRoot

/-!
# Rational root theorem (for usual rational numbers and integers)

This file contains specialization of the rational root theorem -
to use with usual rational numbers and integers.
It (`num_dvd_of_is_root_standard_case` and `den_dvd_of_is_root_standard_case`)
states that for any `p : ℤ[X]` any rational root `r : ℚ` of polynomial
`p.map (Int.castRingHom ℚ)` are such that `r.den ∣ p.leadingCoeff.natAbs`
and `r.num.natAbs ∣ (p.coeff 0).natAbs`.

The file also contains the corresponding integral root theorem for integers
(`root_dvd_of_is_root_of_monic_standard_case`).

## References

 * https://en.wikipedia.org/wiki/Rational_root_theorem
-/

open Polynomial

lemma rat_as_divInt_in_fraction_ring (r : ℚ) :
    r = Rat.divInt (IsFractionRing.num ℤ r : ℤ) (IsFractionRing.den ℤ r : ℤ) := by
  nth_rw 1 [<- IsFractionRing.mk'_num_den ℤ r]
  simp only [IsFractionRing.mk'_eq_div, algebraMap_int_eq, eq_intCast]
  norm_cast

lemma rat_eq_divInt_of_relprimes_aux {r : ℚ} {a b : ℤ}
    (Hb : 0 < b) (H : IsRelPrime a b) (H0 : r = Rat.divInt a b) :
    r.num = a ∧ (r.den : ℤ) = b := by
  apply Rat.div_int_inj (Int.ofNat_lt.mpr (Rat.den_pos r)) Hb r.reduced
  . rw [Nat.Coprime, <- Int.gcd_eq_natAbs]
    rw [<- gcd_isUnit_iff_isRelPrime, Int.isUnit_iff] at H
    simp only [Int.reduceNeg, reduceCtorEq, or_false] at H
    exact (Int.ofNat_inj.mp H)
  . rw [Int.cast_natCast, H0, Rat.num_div_den, Rat.intCast_div_eq_divInt]

lemma nonzero_rat_eq_divInt_of_relprimes {r : ℚ} {a b : ℤ}
    (Hr : r ≠ 0) (H : IsRelPrime a b) (H0 : r = Rat.divInt a b) :
    r.num.natAbs = a.natAbs ∧ r.den = b.natAbs := by
  obtain H1 | H1 | H1 := Int.lt_trichotomy b 0
  . have H2 : r = Rat.divInt (-a) (-b) := by rw [Rat.divInt_neg, neg_neg]; exact H0
    have H3 := rat_eq_divInt_of_relprimes_aux (Int.neg_pos_of_neg H1) (IsRelPrime.neg_neg H) H2
    omega
  . subst b; simp only [Rat.divInt_zero] at H0; exact (Hr H0).elim
  . have H2 := rat_eq_divInt_of_relprimes_aux H1 H H0
    omega

lemma rat_num_abs_and_den_in_fraction_ring (r : ℚ) :
    r.num.natAbs = (IsFractionRing.num ℤ r : ℤ).natAbs ∧
    r.den = (IsFractionRing.den ℤ r : ℤ).natAbs := by
  obtain H | H := eq_or_ne r 0
  . subst r
    simp only [Rat.num_ofNat, Int.natAbs_zero, IsFractionRing.num_zero, Rat.den_ofNat, true_and]
    have H0 := IsFractionRing.isUnit_den_zero (A := ℤ) (K := ℚ)
    obtain H0 | H0 := Int.isUnit_iff.mp H0 <;> simp [H0]
  . exact (nonzero_rat_eq_divInt_of_relprimes H
           (IsFractionRing.num_den_reduced ℤ r) (rat_as_divInt_in_fraction_ring r))

lemma aeval_eq_zero_of_eval_eq_zero {p : ℤ[X]} {r : ℚ}
    (H : eval r (p.map (Int.castRingHom ℚ)) = 0) :
    p.aeval r = 0 := by
  rw [<- eval_map_algebraMap, algebraMap_int_eq]; exact H

/-- **Rational root theorem**, part 1 --/
theorem den_dvd_of_is_root_standard_case {p : ℤ[X]} {r : ℚ}
    (H : r ∈ (p.map (Int.castRingHom ℚ)).roots) :
    r.den ∣ p.leadingCoeff.natAbs := by
  simp only [mem_roots', ne_eq, IsRoot.def] at H; obtain ⟨H, H0⟩ := H
  obtain ⟨d, H1⟩ := den_dvd_of_is_root (aeval_eq_zero_of_eval_eq_zero H0)
  rw [H1, Int.natAbs_mul, (rat_num_abs_and_den_in_fraction_ring r).2]
  apply dvd_mul_right

/-- **Rational root theorem**, part 2 --/
theorem num_dvd_of_is_root_standard_case {p : ℤ[X]} {r : ℚ}
    (H : r ∈ (p.map (Int.castRingHom ℚ)).roots) :
    r.num.natAbs ∣ (p.coeff 0).natAbs := by
  simp only [mem_roots', ne_eq, IsRoot.def] at H
  simp [Int.natAbs_dvd_natAbs]
  obtain ⟨H, H0⟩ := H
  obtain ⟨d, H1⟩ := num_dvd_of_is_root (aeval_eq_zero_of_eval_eq_zero H0)
  rw [H1, <- Int.sign_mul_natAbs r.num, <- Int.sign_mul_natAbs (IsFractionRing.num ℤ r),
      (rat_num_abs_and_den_in_fraction_ring r).1]
  use (d * (IsFractionRing.num ℤ r).sign * r.num.sign)
  ring_nf
  obtain H2 | H2 | H2 := Int.lt_trichotomy r.num 0
  . simp [Int.sign_eq_neg_one_iff_neg.mpr H2]
  . simp only [Rat.num_eq_zero] at H2; subst r; simp
  . simp [Int.sign_eq_one_iff_pos.mpr H2]

/-- **Integral root theorem** --/
theorem root_dvd_of_is_root_of_monic_standard_case {p : ℤ[X]} {n: ℤ}
    (H : p.Monic) (H0 : n ∈ p.roots) :
    n.natAbs ∣ (p.coeff 0).natAbs := by
  have H1 : (n : ℚ) ∈ (p.map (Int.castRingHom ℚ)).roots := by
    simp only [mem_roots', ne_eq, IsRoot.def] at H0
    simp [map_monic_ne_zero H, H0.2]
  have H2 : (n : ℚ).num = n := by rfl
  rw [<- H2]
  exact num_dvd_of_is_root_standard_case H1


--- Example of use

example (r : ℚ) (H : r ∈ (2 * X ^ 3 + 3 * X ^ 2 - 3 : ℚ[X]).roots) :
    r.den ∣ 2 ∧ r.num.natAbs ∣ 3 := by
  have H0 : (2 * X ^ 3 + 3 * X ^ 2 - 3 : ℚ[X]) =
            (2 * X ^ 3 + 3 * X ^ 2 - 3 : ℤ[X]).map (Int.castRingHom ℚ) := by simp
  have H1 : (2 * X ^ 3 + 3 * X ^ 2 - 3: ℤ[X]).natDegree = 3 := by compute_degree!
  rw [H0] at H; constructor
  . apply den_dvd_of_is_root_standard_case at H
    unfold leadingCoeff at H; rw [H1] at H; simp at H; exact H
  . apply num_dvd_of_is_root_standard_case at H
    simp at H; exact H

[Ilmārs Cīrulis]

Thank you! :heart:

Tomorrow will take more serious look at your approach (from which I took the proof of aux6 which I couldn't prove :sweat_smile:), but now falling asleep. :bed:

[Ilmārs Cīrulis]

Forgot to ask.
Is such result useful enough to put it in Mathlib? What do you think?

(It's just that the existing Rational Root Theorem is impressively general and for this reason difficult to use in the standard case of rational root and integer coefficients (at least for me).)