The singular-point correction in the finite-field curve estimate. The remaining estimate for all nonsingular rational points is not asserted here.
theorem
CCDN.pderiv_totalDegree_le
{K : Type u_1}
{σ : Type u_2}
[Field K]
(f : MvPolynomial σ K)
(i : σ)
:
A partial derivative lowers the total degree by at least one.
theorem
CCDN.not_dvd_pderiv_of_pderiv_ne_zero
{K : Type u_1}
{σ : Type u_2}
[Field K]
{f : MvPolynomial σ K}
(hf : f ≠ 0)
{i : σ}
(hi : (MvPolynomial.pderiv i) f ≠ 0)
:
A nonzero polynomial does not divide any of its nonzero partial derivatives, since these have smaller total degree.
theorem
CCDN.plane_singular_points_card_le
{K : Type u_1}
{ι : Type u_2}
[Field K]
[Fintype ι]
{p : ℕ}
[CharP K p]
(f : MvPolynomial (Fin 2) K)
(hf : Irreducible f)
(hpos : 0 < f.totalDegree)
(hchar : f.totalDegree < p)
(z : ι → Fin 2 → K)
(hz : Function.Injective z)
(hzf : ∀ (i : ι), (MvPolynomial.eval (z i)) f = 0)
(hzsing : ∀ (i : ι) (j : Fin 2), (MvPolynomial.eval (z i)) ((MvPolynomial.pderiv j) f) = 0)
:
Distinct singular points of an irreducible plane equation of degree d
number at most d(d-1), whenever the degree is smaller than the characteristic.