Grace/Cumulus/Algebra/Field/AlgebraicClosure.g17

Open in Workbench Download source

Imports

Algebraic

Declarations

• IsAlgebraicallyClosed predicate
• IsAlgebraicallyClosed.field theorem derivation
• IsAlgebraicallyClosed.root theorem derivation

Source

1-- Algebraic closedness as the usual monic-polynomial root property.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 Grace.Cumulus.Algebra.Field.AlgebraicClosure8import Algebraic910-- A coefficient list of length n represents a monic polynomial of degree n.11-- The empty list represents 1 and is excluded from the root requirement.12predicate IsAlgebraicallyClosed (A add zero neg mul one : Set) :=13  IsField(A, add, zero, neg, mul, one) ∧14  (∀ cs, List(A, cs) → cs ≠ [] → ∃ x ∈ A, monicValue{A}(identity(A), add, mul, one, x, cs) = zero)1516notation scoped IsAlgebraicallyClosed(R) => IsAlgebraicallyClosed(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)1718theorem IsAlgebraicallyClosed.field (A add zero neg mul one : Set)19  requires closed : IsAlgebraicallyClosed(A, add, zero, neg, mul, one)20  shows IsField(A, add, zero, neg, mul, one)21proof22  exact closed.left2324theorem IsAlgebraicallyClosed.root (A add zero neg mul one : Set) (cs : List(A))25  requires closed : IsAlgebraicallyClosed(A, add, zero, neg, mul, one)26  requires nonconstant : cs ≠ []27  shows ∃ x ∈ A, monicValue{A}(identity(A), add, mul, one, x, cs) = zero28proof29  exact closed.right with cs, nonconstant30