A real polynomial of odd degree has a real root
ProvedMetodosNumericos.odd_degree_real_rootIf a polynomial with real coefficients has odd degree, then it has a real root. This is Proposição 4.1.2, which the source deduces from the conjugate-pair statement and the fundamental theorem of algebra.
import Mathlib
namespace MetodosNumericos
theorem odd_degree_real_root (p : Polynomial ℝ) (hodd : Odd p.natDegree) :
∃ x : ℝ, p.eval x = 0 := 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 real coefficients (Mathlib's polynomial type over ), the hypothesis is that its natural-number degree is odd, and the conclusion is that there exists a real number with .
The degree used is the natural-number degree, which is for the zero polynomial; since is not odd, the hypothesis excludes and forces the degree to be at least . The root is asserted to exist, with no claim about uniqueness or multiplicity.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.