Simple roots of squarefree polynomials #
A squarefree polynomial has nonzero derivative at every root in its coefficient ring.
This supplies the pointwise simple-root premise of TauCeti.Sturm.IsAlternating.sum_sign,
which requires p.derivative.eval r ≠ 0 at each root r in the interval.
The file also records that -(X ^ 2 + 1) is squarefree over a field of characteristic other than
two, the polynomial of the conic x ^ 2 + y ^ 2 + 1 = 0 in the form y ^ 2 = f(x).
theorem
Squarefree.eval_derivative_ne_zero
{R : Type u_1}
[CommRing R]
[Nontrivial R]
{p : Polynomial R}
(hp : Squarefree p)
{x : R}
(hx : Polynomial.eval x p = 0)
:
A squarefree polynomial has nonzero derivative at every root in its coefficient ring.
theorem
TauCeti.Polynomial.squarefree_neg_X_sq_add_one
{k : Type u_1}
[Field k]
(h2 : 2 ≠ 0)
:
Squarefree (-(Polynomial.X ^ 2 + 1))
-(X ^ 2 + 1) is squarefree over a field in which 2 ≠ 0: X ^ 2 + 1 = X ^ 2 - C (-1) is
separable there.