diff --git a/Everything/Safe.agda b/Everything/Safe.agda index 014ed6d..abf4a1b 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -85,6 +85,7 @@ open import Rings.Divisible.Lemmas open import Rings.Associates.Lemmas open import Rings.InitialRing open import Rings.Homomorphisms.Lemmas +open import Rings.UniqueFactorisationDomains.Definition open import Setoids.Setoids open import Setoids.DirectSum @@ -125,9 +126,6 @@ open import Monoids.Definition open import Semirings.Definition open import Semirings.Solver -open import Fields.CauchyCompletion.Group -open import Fields.CauchyCompletion.Ring - open import Categories.Definition open import Categories.Functor.Definition open import Categories.Functor.Lemmas @@ -149,4 +147,7 @@ open import Modules.PolynomialModule open import Modules.Lemmas open import Modules.DirectSum +open import Fields.CauchyCompletion.Ring +open import Fields.CauchyCompletion.Comparison + module Everything.Safe where diff --git a/Fields/CauchyCompletion/Addition.agda b/Fields/CauchyCompletion/Addition.agda index f03c0ff..d7b25a5 100644 --- a/Fields/CauchyCompletion/Addition.agda +++ b/Fields/CauchyCompletion/Addition.agda @@ -32,9 +32,10 @@ open import Fields.CauchyCompletion.Definition order F open import Rings.Orders.Partial.Lemmas pRing open import Rings.Orders.Total.Lemmas order -lemm : (m : ℕ) (a b : Sequence A) → index (apply _+_ a b) m ≡ (index a m) + (index b m) -lemm zero a b = refl -lemm (succ m) a b = lemm m (Sequence.tail a) (Sequence.tail b) +private + lemm : (m : ℕ) (a b : Sequence A) → index (apply _+_ a b) m ≡ (index a m) + (index b m) + lemm zero a b = refl + lemm (succ m) a b = lemm m (Sequence.tail a) (Sequence.tail b) _+C_ : CauchyCompletion → CauchyCompletion → CauchyCompletion CauchyCompletion.elts (record { elts = a ; converges = convA } +C record { elts = b ; converges = convB }) = apply _+_ a b diff --git a/Fields/CauchyCompletion/Approximation.agda b/Fields/CauchyCompletion/Approximation.agda index acd2801..f7d7f95 100644 --- a/Fields/CauchyCompletion/Approximation.agda +++ b/Fields/CauchyCompletion/Approximation.agda @@ -40,20 +40,26 @@ open import Fields.CauchyCompletion.Comparison order F charNot2 abstract chain : {a b : A} (c : CauchyCompletion) → (a r