-- Algebraic closedness as the usual monic-polynomial root property.
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Field.AlgebraicClosure
import Algebraic

-- A coefficient list of length n represents a monic polynomial of degree n.
-- The empty list represents 1 and is excluded from the root requirement.
predicate IsAlgebraicallyClosed (A add zero neg mul one : Set) :=
  IsField(A, add, zero, neg, mul, one) ∧
  (∀ cs, List(A, cs) → cs ≠ [] → ∃ x ∈ A, monicValue{A}(identity(A), add, mul, one, x, cs) = zero)

notation scoped IsAlgebraicallyClosed(R) => IsAlgebraicallyClosed(R.carrier, R.add, R.zero, R.neg, R.mul, R.one)

theorem IsAlgebraicallyClosed.field (A add zero neg mul one : Set)
  requires closed : IsAlgebraicallyClosed(A, add, zero, neg, mul, one)
  shows IsField(A, add, zero, neg, mul, one)
proof
  exact closed.left

theorem IsAlgebraicallyClosed.root (A add zero neg mul one : Set) (cs : List(A))
  requires closed : IsAlgebraicallyClosed(A, add, zero, neg, mul, one)
  requires nonconstant : cs ≠ []
  shows ∃ x ∈ A, monicValue{A}(identity(A), add, mul, one, x, cs) = zero
proof
  exact closed.right with cs, nonconstant