Smooth points on irreducible hypersurfaces over an algebraically closed field. The characteristic bound supplies a nonzero partial derivative; the Nullstellensatz supplies a point where it does not vanish.

theorem CCDN.exists_hypersurface_point_eval_ne_zero {K : Type u_1} {σ : Type u_2} [Field K] [IsAlgClosed K] [Finite σ] (f g : MvPolynomial σ K) (hf : Irreducible f) (hg : ¬f ∣ g) : ∃ (z : σ → K), (MvPolynomial.eval z) f = 0 ∧ (MvPolynomial.eval z) g ≠ 0

A polynomial outside a prime hypersurface ideal is nonzero at some point of that hypersurface over an algebraically closed field.

theorem CCDN.exists_smooth_hypersurface_point_of_degree_lt_char {K : Type u_1} {σ : Type u_2} [Field K] [IsAlgClosed K] [Finite σ] (f : MvPolynomial σ K) (hf : Irreducible f) (hpos : 0 < f.totalDegree) (hchar : CharZeroOrGT K f.totalDegree) : ∃ (z : σ → K) (j : σ), (MvPolynomial.eval z) f = 0 ∧ (MvPolynomial.eval z) ((MvPolynomial.pderiv j) f) ≠ 0

An irreducible hypersurface of positive degree smaller than the characteristic (or in characteristic zero) has a smooth rational point over the algebraically closed base.