AlgebraicallyClosedFields

Algebraically closed fields cannot be finite: a foundational ZF example

Open in Workbench View on GitHub

1-- Algebraically closed fields cannot be finite: a foundational ZF example.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module AlgebraicallyClosedFields8import Grace.Cumulus.Algebra.Field.Infinite910section Fields11variable (A add zero neg mul one : Set)12notation ring R := (A, add, zero, neg, mul, one)1314theorem infinite15  requires closed : IsAlgebraicallyClosed(R)16  shows ¬Finite(R)17proof18  exact IsAlgebraicallyClosed.infinite with *1920-- The reusable polynomial construction needs only a commutative ring.21-- A nonempty lower-coefficient list ensures that the polynomial is nonconstant.22theorem vanishing (xs : List(A))23  requires ring : IsCommRing(R)24  shows ∃ c ∈ R, ∃ cs, List(A, cs) ∧ (∀ x ∈ R, x ∈ listSupport{A}(xs) → hornerAt{A}(add, mul, one, x, c :: cs) = R[0])25proof26  exact hornerAt.monic_vanishing_on_list with *2728end Fields29