{-# OPTIONS --cubical --no-import-sorts --allow-unsolved-metas #-} module AFF2024.Algebra.PolynomialVanishing where open import Cubical.Foundations.Prelude open import Cubical.HITs.PropositionalTruncation open import Cubical.HITs.PropositionalTruncation.Monad open import Cubical.Data.Sigma open import Cubical.Data.Nat hiding (elim) open import Cubical.Data.Vec hiding (length) open import Cubical.Algebra.CommRing open import Cubical.Algebra.Polynomials.UnivariateList.Base open import Data.List open import Data.List.Relation.Unary.All open import Data.List.Relation.Unary.AllPairs open import AFF2024.Basics open import AFF2024.Algebra.Basics module _ {ℓ : Level} (R…@(R , Rstr) : CommRing ℓ) where open CommRingStr Rstr open Degree R… open Apartness R… open PolyMod R… hiding (0r) lemma : {n : ℕ} (f : Poly R…) → HasDegree≤ f n → (xs : List R) → length xs ≡ n → All (λ x → eval f x ≡ 0r) xs → AllPairs _##_ xs → f ≡ 0P lemma = {!!} module _ (inf : Infinite R _##_) where lemma' : (f : Poly R…) → ((x : R) → eval f x ≡ 0r) → f ≡ 0P lemma' f p = elim (λ _ → isSetPoly _ _) (λ e → e) do (n , deg≤n) ← degreeBound f (xs , len , q) ← takeFrom∞ inf n return (lemma f deg≤n xs len (allP p xs) q) corollary : (n : ℕ) (f : MultivariatePoly R… n) → ((xs : Vec R n) → evalT f xs ≡ 0r) → f ≡ const n 0r corollary n f p = {!!}