diff --git a/Everything/Safe.agda b/Everything/Safe.agda index 027c39d..44d80c4 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -47,7 +47,7 @@ open import Rings.Lemmas open import Rings.Orders.Partial.Definition open import Rings.Orders.Total.Lemmas open import Rings.Orders.Partial.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Rings.DirectSum open import Rings.Polynomial.Ring open import Rings.Polynomial.Evaluation @@ -55,6 +55,17 @@ open import Rings.Ideals.Definition open import Rings.Isomorphisms.Definition open import Rings.Quotients.Definition open import Rings.Cosets +open import Rings.EuclideanDomains.Definition +open import Rings.EuclideanDomains.Examples +open import Rings.Homomorphisms.Image +open import Rings.Homomorphisms.Kernel +open import Rings.Ideals.FirstIsomorphismTheorem +open import Rings.Ideals.Lemmas +open import Rings.Ideals.Prime.Definition +open import Rings.Ideals.Principal.Definition +open import Rings.IntegralDomains.Examples +open import Rings.PrincipalIdealDomain +open import Rings.Subrings.Definition open import Setoids.Setoids open import Setoids.DirectSum diff --git a/Fields/FieldOfFractions/Addition.agda b/Fields/FieldOfFractions/Addition.agda index 3f91267..04a0b5e 100644 --- a/Fields/FieldOfFractions/Addition.agda +++ b/Fields/FieldOfFractions/Addition.agda @@ -6,7 +6,7 @@ open import Groups.Definition open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids @@ -25,8 +25,7 @@ fieldOfFractionsPlus (a ,, (b , b!=0)) (c ,, (d , d!=0)) = (((a * d) + (b * c)) open Ring R ans : ((b * d) ∼ Ring.0R R) → False ans pr with IntegralDomain.intDom I pr - ans pr | inl x = b!=0 x - ans pr | inr x = d!=0 x + ans pr | f = exFalso (d!=0 (f b!=0)) plusWellDefined : {a b c d : fieldOfFractionsSet} → (Setoid._∼_ fieldOfFractionsSetoid a c) → (Setoid._∼_ fieldOfFractionsSetoid b d) → Setoid._∼_ fieldOfFractionsSetoid (fieldOfFractionsPlus a b) (fieldOfFractionsPlus c d) plusWellDefined {a ,, (b , b!=0)} {c ,, (d , d!=0)} {e ,, (f , f!=0)} {g ,, (h , h!=0)} af=be ch=dg = need diff --git a/Fields/FieldOfFractions/Field.agda b/Fields/FieldOfFractions/Field.agda index b5b5ec6..441be2a 100644 --- a/Fields/FieldOfFractions/Field.agda +++ b/Fields/FieldOfFractions/Field.agda @@ -6,7 +6,7 @@ open import Groups.Definition open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids diff --git a/Fields/FieldOfFractions/Group.agda b/Fields/FieldOfFractions/Group.agda index c73d7d7..1fee587 100644 --- a/Fields/FieldOfFractions/Group.agda +++ b/Fields/FieldOfFractions/Group.agda @@ -6,7 +6,7 @@ open import Groups.Definition open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids diff --git a/Fields/FieldOfFractions/Lemmas.agda b/Fields/FieldOfFractions/Lemmas.agda index 979d4e0..f352b4c 100644 --- a/Fields/FieldOfFractions/Lemmas.agda +++ b/Fields/FieldOfFractions/Lemmas.agda @@ -8,7 +8,7 @@ open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas open import Rings.Homomorphisms.Definition -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids diff --git a/Fields/FieldOfFractions/Multiplication.agda b/Fields/FieldOfFractions/Multiplication.agda index 14911d5..1c075df 100644 --- a/Fields/FieldOfFractions/Multiplication.agda +++ b/Fields/FieldOfFractions/Multiplication.agda @@ -6,7 +6,7 @@ open import Groups.Definition open import Groups.Lemmas open import Rings.Definition open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids @@ -25,8 +25,7 @@ fieldOfFractionsTimes (a ,, (b , b!=0)) (c ,, (d , d!=0)) = (a * c) ,, ((b * d) open Ring R ans : ((b * d) ∼ Ring.0R R) → False ans pr with IntegralDomain.intDom I pr - ans pr | inl x = b!=0 x - ans pr | inr x = d!=0 x + ans pr | f = exFalso (d!=0 (f b!=0)) fieldOfFractionsTimesWellDefined : {a b c d : fieldOfFractionsSet} → (Setoid._∼_ fieldOfFractionsSetoid a c) → (Setoid._∼_ fieldOfFractionsSetoid b d) → (Setoid._∼_ fieldOfFractionsSetoid (fieldOfFractionsTimes a b) (fieldOfFractionsTimes c d)) fieldOfFractionsTimesWellDefined {a ,, (b , _)} {c ,, (d , _)} {e ,, (f , _)} {g ,, (h , _)} af=be ch=dg = need diff --git a/Fields/FieldOfFractions/Order.agda b/Fields/FieldOfFractions/Order.agda index 22b37eb..c1c9cad 100644 --- a/Fields/FieldOfFractions/Order.agda +++ b/Fields/FieldOfFractions/Order.agda @@ -9,7 +9,7 @@ open import Rings.Orders.Partial.Definition open import Rings.Orders.Total.Definition open import Rings.Orders.Total.Lemmas open import Rings.Lemmas -open import Rings.IntegralDomains +open import Rings.IntegralDomains.Definition open import Fields.Fields open import Functions open import Setoids.Setoids @@ -20,698 +20,694 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_) module Fields.FieldOfFractions.Order {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {_} {c} A} {pOrder : SetoidPartialOrder S _<_} {pRing : PartiallyOrderedRing R pOrder} (I : IntegralDomain R) (order : TotallyOrderedRing pRing) where - open import Fields.FieldOfFractions.Setoid I - open import Fields.FieldOfFractions.Ring I +open import Fields.FieldOfFractions.Setoid I +open import Fields.FieldOfFractions.Ring I - open SetoidTotalOrder (TotallyOrderedRing.total order) - open import Rings.Orders.Partial.Lemmas - open PartiallyOrderedRing pRing +open SetoidTotalOrder (TotallyOrderedRing.total order) +open import Rings.Orders.Partial.Lemmas +open PartiallyOrderedRing pRing - fieldOfFractionsComparison : Rel fieldOfFractionsSet - fieldOfFractionsComparison (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) with totality (Ring.0R R) denomA - fieldOfFractionsComparison (numA ,, (denomA , denomA!=0)) (numB ,, (denomB , denomB!=0)) | inl (inl 0