ComplexFundamentalTheorem

FTA and concrete weak Nullstellensatz: no algebraic-closure premise

Open in Workbench View on GitHub

1-- FTA and concrete weak Nullstellensatz: no algebraic-closure premise.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module ComplexFundamentalTheoremExample8import Grace.Cumulus.Complex.Nullstellensatz910section Complexes11notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)1213theorem root_exists (cs : List(ℂ))14  requires nonconstant : cs ≠ []15  shows ∃ a ∈ ℂ, complexPolynomial(cs)(a) = ℂ[0]16proof17  exact complexPolynomial.has_root at cs with *1819theorem square_root (b : Set)20  requires member : b ∈ ℂ21  shows ∃ a ∈ ℂ, ℂ[a * a] = b22proof23  exact complex.square_root at b with *2425section Polynomials26variable (I G : Set)27notation ring P := ℂ[I]28hypothesis finite : Finite(I)29hypothesis generators : G ⊆ P3031theorem no_common_zero_iff_unit32  shows P[1] ∈ idealSpan(P, G) ↔ ¬(∃ v, PolynomialCommonZero(I, ℂ, G, v))33proof34  exact complexes.weak_nullstellensatz at I, G with *3536theorem no_common_zero_iff_certificate37  shows (∃ terms, List(idealProducts(P, G), terms) ∧ P[1] = ringSum{idealProducts(P, G)}(polynomialAdd(I, ℂ), P[0], terms)) ↔ ¬(∃ v, PolynomialCommonZero(I, ℂ, G, v))38proof39  exact complexes.unsatisfiable_iff_certificate at I, G with *4041end Polynomials42end Complexes43