Rational root test: and
ProvedMetodosNumericos.rational_rootIf a polynomial with integer coefficients has a rational root in lowest terms, then the numerator divides the constant coefficient and the denominator divides the leading coefficient. This is Proposição 4.3.1, the test the source uses to enumerate the rational candidates before any iterative method is started.
import Mathlib
namespace MetodosNumericos
theorem rational_root (p : Polynomial ℤ) (hp : p ≠ 0) (r : ℚ)
(hr : Polynomial.aeval r p = 0) :
r.num ∣ p.coeff 0 ∧ (r.den : ℤ) ∣ p.leadingCoeff := by sorry
end MetodosNumericosRead-back
What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)
Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context.
For a polynomial with integer coefficients and a rational number , the hypotheses are that is not the zero polynomial and that evaluating at (in , via the canonical ring map) gives . The conclusion is the conjunction of two divisibilities in :
- the numerator of divides the coefficient of of ;
- the denominator of , viewed as an integer, divides the leading coefficient of .
Here is Mathlib's rational number type, whose numerator and denominator are by construction coprime with positive denominator, so "in lowest terms" is automatic. The constant coefficient may be , in which case the first divisibility is trivially true.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.