Sharp bounds for distinct points in proper polynomial sections. In the plane, the principal Hilbert function gives the usual product-of-degrees bound.

theorem CCDN.plane_common_zeros_card_le {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] (f g : MvPolynomial (Fin 2) K) (hf : Irreducible f) (hfg : ¬f ∣ g) (z : ι → Fin 2 → K) (hz : Function.Injective z) (hzf : ∀ (i : ι), (MvPolynomial.eval (z i)) f = 0) (hzg : ∀ (i : ι), (MvPolynomial.eval (z i)) g = 0) : Fintype.card ι ≤ f.totalDegree * g.totalDegree

An irreducible plane curve and a polynomial not divisible by its equation have at most the product of their degrees many distinct common zeros.

theorem CCDN.count_curve_section_le {n d : ℕ} (I : Ideal (CoordinatePolynomial n)) [I.IsPrime] (hd : HasAffineCurveDegree I d) (g : CoordinatePolynomial n) (hg : g ∉ I) (B : ℝ) : count (idealZeroLocus I ∩ zeroLocus g) B ≤ d * MvPolynomial.totalDegree g

The section bound directly in the real-radius integer counting interface.