At the degree of the irreducible image equation, the plane relation space is one-dimensional. This supplies the specialized-kernel condition for first-order deformation of a degree-preserving projection.

theorem CCDN.eq_scalar_mul_of_dvd_of_totalDegree_le {K : Type u_1} {σ : Type u_2} [Field K] (f g : MvPolynomial σ K) (hf : f ≠ 0) (hdiv : f ∣ g) (hdeg : g.totalDegree ≤ f.totalDegree) : ∃ (c : K), g = c • f

A multiple g of a nonzero polynomial f with total degree at most that of f is a scalar multiple of f.

theorem CCDN.plane_projection_relation_space {K : Type u_1} {τ : Type u_2} [Field K] (I : Ideal (MvPolynomial τ K)) (a : Fin 2 → MvPolynomial τ K) (f : MvPolynomial (Fin 2) K) (hf : f ≠ 0) (hker : ∀ (g : MvPolynomial (Fin 2) K), (MvPolynomial.aeval a) g ∈ I ↔ f ∣ g) (g : MvPolynomial (Fin 2) K) (hg : g.totalDegree ≤ f.totalDegree) (hzero : (MvPolynomial.aeval a) g ∈ I) : ∃ (c : K), g = c • f

Every relation no larger than the image equation is its scalar multiple.