-- Fundamental theorem of algebra for the concrete real-pair complex field.
-- 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.Complex.FundamentalTheorem
import PowerDirections
import Algebra.Field.AlgebraicClosure

section Complexes
notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)

theorem complexes.fundamental_theorem_of_algebra (cs : List(ℂ))
  requires nonconstant : cs ≠ []
  shows ∃ a ∈ ℂ, monicValue(ℂ, identity(ℂ), ℂ, a, cs) = ℂ[0]
proof
  have directions : ∀ n ∈ ℕ, ∀ z ∈ ℂ, ∀ w ∈ ℂ, z ≠ ℂ[0] → w ≠ ℂ[0] →
    ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ succ(n) * w]) < realZero
    intros n nIn z zIn w wIn nonzeroZ nonzeroW
    have nNat := nat.omega.backward at n with *
    exact complexDot.power_direction with *
  exact complexPolynomial.root_of_power_directions with *

-- The usual function-evaluation form of FTA for a nonconstant monic polynomial.
theorem complexPolynomial.has_root (cs : List(ℂ))
  requires nonconstant : cs ≠ []
  shows ∃ a ∈ ℂ, complexPolynomial(cs)(a) = ℂ[0]
proof
  obtain ⟨a, member, root⟩ := complexes.fundamental_theorem_of_algebra at cs with *
  refine ⟨a, member, ?_⟩
  rwa complexPolynomial.value

theorem complexes.algebraically_closed
  shows IsAlgebraicallyClosed(ℂ)
proof
  unfold IsAlgebraicallyClosed
  refine ⟨complexes.is_field, ?_⟩
  intros cs list nonconstant
  exact complexes.fundamental_theorem_of_algebra with *

end Complexes