AlgebraicClosure.spanEval_ne_top

theorem AlgebraicClosure.spanEval_ne_top : ∀ (k : Type u) [inst : Field k], AlgebraicClosure.spanEval k ≠ ⊤

The theorem `AlgebraicClosure.spanEval_ne_top` states that for any type `k` which has a field structure, the span of the evaluation of `x_f` across monic irreducible polynomials `f`, where `x_f` is an indeterminate, is not equal to the whole ideal (denoted by `⊤`) of the multivariable polynomial over the algebraic closure of monic irreducible polynomials over `k`. In other words, the set of all values obtained by evaluating `x_f` across all monic irreducible polynomials `f` does not span the entire ideal in the multivariate polynomial ring.

More concisely: For any field `k`, the span of evaluations of an indeterminate `x_f` over monic irreducible polynomials `f` does not equal the whole ideal in the multivariate polynomial ring over the algebraic closure of `k`.