Coefficient-linear descent detects nonmembership in scalar-extended ideals, and descends degree-bounded separating equations.

theorem CCDN.mem_ideal_scalar_extension_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) K)) (f : MvPolynomial (Fin n) K) : (MvPolynomial.map (algebraMap K L)) f ∈ Ideal.map (MvPolynomial.map (algebraMap K L)) I ↔ f ∈ I

For a field extension L of K, a polynomial f over K lies in the extension of the ideal I to polynomials over L if and only if f lies in I.

theorem CCDN.exists_polynomialCoefficientLinear_not_mem {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {n : ℕ} (J : Ideal (MvPolynomial (Fin n) K)) (g : MvPolynomial (Fin n) L) (hg : g ∉ Ideal.map (MvPolynomial.map (algebraMap K L)) J) : ∃ (φ : L →ₗ[K] K), (polynomialCoefficientLinear φ) g ∉ J

Some coefficient functional detects nonmembership in an extended ideal.