Grace/Cumulus/Complex/FundamentalTheorem.g17

Open in Workbench Download source

Imports

PowerDirections · Algebra.Field.AlgebraicClosure

Declarations

• complexes.fundamental_theorem_of_algebra theorem derivation
• complexPolynomial.has_root theorem derivation
• complexes.algebraically_closed theorem derivation

Source

1-- Fundamental theorem of algebra for the concrete real-pair complex field.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.Complex.FundamentalTheorem8import PowerDirections9import Algebra.Field.AlgebraicClosure1011section Complexes12notation ring ℂ := (complexCarrier, complexAdd, complexZero, complexNeg, complexMul, complexOne)1314theorem complexes.fundamental_theorem_of_algebra (cs : List(ℂ))15  requires nonconstant : cs ≠ []16  shows ∃ a ∈ ℂ, monicValue(ℂ, identity(ℂ), ℂ, a, cs) = ℂ[0]17proof18  have directions : ∀ n ∈ ℕ, ∀ z ∈ ℂ, ∀ w ∈ ℂ, z ≠ ℂ[0] → w ≠ ℂ[0] →19    ∃ u ∈ ℂ, Euclidean.dot(z, ℂ[u ^ succ(n) * w]) < realZero20    intros n nIn z zIn w wIn nonzeroZ nonzeroW21    have nNat := nat.omega.backward at n with *22    exact complexDot.power_direction with *23  exact complexPolynomial.root_of_power_directions with *2425-- The usual function-evaluation form of FTA for a nonconstant monic polynomial.26theorem complexPolynomial.has_root (cs : List(ℂ))27  requires nonconstant : cs ≠ []28  shows ∃ a ∈ ℂ, complexPolynomial(cs)(a) = ℂ[0]29proof30  obtain ⟨a, member, root⟩ := complexes.fundamental_theorem_of_algebra at cs with *31  refine ⟨a, member, ?_⟩32  rwa complexPolynomial.value3334theorem complexes.algebraically_closed35  shows IsAlgebraicallyClosed(ℂ)36proof37  unfold IsAlgebraicallyClosed38  refine ⟨complexes.is_field, ?_⟩39  intros cs list nonconstant40  exact complexes.fundamental_theorem_of_algebra with *4142end Complexes43