From 8377c23613954171ef7ef99c6d5d05598a3c5f60 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <smaug451@gmail.com>
Date: Sun, 17 Nov 2019 17:37:10 +0000
Subject: [PATCH] Polynomial ring (#76)

---
 Everything/Safe.agda                          |   4 +
 Fields/FieldOfFractions/Lemmas.agda           |   1 +
 Groups/Polynomials/Addition.agda              |  61 +++++
 Groups/Polynomials/Definition.agda            | 131 +++++++++
 Groups/Polynomials/Examples.agda              |  35 +++
 Groups/Polynomials/Group.agda                 |  81 ++++++
 Lists/Lists.agda                              | 254 ++++++++++--------
 Numbers/Integers/Definition.agda              |  16 ++
 Numbers/Integers/Integers.agda                |   4 +-
 Numbers/Integers/Multiplication.agda          | 173 ------------
 Numbers/Integers/Order.agda                   |   4 +-
 .../RingStructure/IntegralDomain.agda         |  23 ++
 Numbers/Integers/RingStructure/Ring.agda      | 179 ++++++++++++
 Numbers/Naturals/Definition.agda              |   8 +
 Numbers/Rationals/Lemmas.agda                 |   1 +
 Rings/Definition.agda                         |  67 ++---
 Rings/Homomorphisms/Definition.agda           |  26 ++
 Rings/Ideals/Definition.agda                  |  20 ++
 Rings/Isomorphisms/Definition.agda            |  22 ++
 Rings/Polynomial/Definition.agda              |  33 +++
 Rings/Polynomial/Multiplication.agda          | 123 +++++++++
 Rings/Polynomial/Ring.agda                    |  45 ++++
 Vectors.agda                                  |  14 +-
 23 files changed, 984 insertions(+), 341 deletions(-)
 create mode 100644 Groups/Polynomials/Addition.agda
 create mode 100644 Groups/Polynomials/Definition.agda
 create mode 100644 Groups/Polynomials/Examples.agda
 create mode 100644 Groups/Polynomials/Group.agda
 create mode 100644 Numbers/Integers/RingStructure/IntegralDomain.agda
 create mode 100644 Numbers/Integers/RingStructure/Ring.agda
 create mode 100644 Rings/Homomorphisms/Definition.agda
 create mode 100644 Rings/Ideals/Definition.agda
 create mode 100644 Rings/Isomorphisms/Definition.agda
 create mode 100644 Rings/Polynomial/Definition.agda
 create mode 100644 Rings/Polynomial/Multiplication.agda
 create mode 100644 Rings/Polynomial/Ring.agda

diff --git a/Everything/Safe.agda b/Everything/Safe.agda
index fc6500e..1440529 100644
--- a/Everything/Safe.agda
+++ b/Everything/Safe.agda
@@ -29,6 +29,7 @@ open import Groups.SymmetricGroups.Lemmas
 open import Groups.ActionIsSymmetry
 open import Groups.Cyclic.Definition
 open import Groups.Cyclic.DefinitionLemmas
+open import Groups.Polynomials.Examples
 
 open import Fields.Fields
 open import Fields.Orders.Partial.Definition
@@ -45,6 +46,9 @@ open import Rings.Orders.Total.Lemmas
 open import Rings.Orders.Partial.Lemmas
 open import Rings.IntegralDomains
 open import Rings.DirectSum
+open import Rings.Polynomial.Ring
+open import Rings.Ideals.Definition
+open import Rings.Isomorphisms.Definition
 
 open import Setoids.Setoids
 open import Setoids.DirectSum
diff --git a/Fields/FieldOfFractions/Lemmas.agda b/Fields/FieldOfFractions/Lemmas.agda
index 021ad2d..979d4e0 100644
--- a/Fields/FieldOfFractions/Lemmas.agda
+++ b/Fields/FieldOfFractions/Lemmas.agda
@@ -7,6 +7,7 @@ open import Groups.Definition
 open import Groups.Lemmas
 open import Rings.Definition
 open import Rings.Lemmas
+open import Rings.Homomorphisms.Definition
 open import Rings.IntegralDomains
 open import Fields.Fields
 open import Functions
diff --git a/Groups/Polynomials/Addition.agda b/Groups/Polynomials/Addition.agda
new file mode 100644
index 0000000..c977e77
--- /dev/null
+++ b/Groups/Polynomials/Addition.agda
@@ -0,0 +1,61 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Definition
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Vectors
+open import Lists.Lists
+open import Maybe
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Groups.Polynomials.Addition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where
+
+open import Groups.Polynomials.Definition G
+open Setoid S
+open Equivalence eq
+open Group G
+
+_+P_ : NaivePoly → NaivePoly → NaivePoly
+_+P_ = listZip _+_ id id
+
+PidentRight : {m : NaivePoly} → polysEqual (m +P []) m
+PidentRight {[]} = record {}
+PidentRight {x :: m} = reflexive ,, identityOfIndiscernablesLeft polysEqual (Equivalence.reflexive (Setoid.eq naivePolySetoid)) (equalityCommutative (mapId m))
+
++PwellDefined : {m n x y : NaivePoly} → polysEqual m x → polysEqual n y → polysEqual (m +P n) (x +P y)
++PwellDefined {[]} {[]} {[]} {[]} m=x n=y = record {}
++PwellDefined {[]} {[]} {[]} {x :: y} m=x (fst ,, snd) = fst ,, identityOfIndiscernablesRight polysEqual snd (equalityCommutative (mapId y))
++PwellDefined {[]} {[]} {x :: xs} {[]} (fst ,, snd) n=y = fst ,, identityOfIndiscernablesRight polysEqual snd (equalityCommutative (mapId xs))
++PwellDefined {[]} {[]} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identRight ,, +PwellDefined {[]} {[]} {xs} {ys} snd snd2
++PwellDefined {[]} {n :: ns} {[]} {[]} m=x (fst ,, snd) = fst ,, identityOfIndiscernablesLeft polysEqual snd (equalityCommutative (mapId ns))
++PwellDefined {[]} {n :: ns} {[]} {y :: ys} m=x (fst ,, snd) = fst ,, +PwellDefined m=x snd
++PwellDefined {[]} {n :: ns} {x :: xs} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive fst2 (symmetric fst) ,, ans
+  where
+    ans : polysEqual (map (λ z → z) ns) (map (λ z → z) xs)
+    ans rewrite mapId ns | mapId xs = Equivalence.transitive (Setoid.eq naivePolySetoid) snd2 snd
++PwellDefined {[]} {n :: ns} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric identLeft) (+WellDefined (symmetric fst) fst2) ,, (+PwellDefined snd snd2)
++PwellDefined {m :: ms} {[]} {[]} {[]} (fst ,, snd) _ = fst ,, identityOfIndiscernablesLeft polysEqual snd (equalityCommutative (mapId ms))
++PwellDefined {m :: ms} {[]} {[]} {x :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive fst (symmetric fst2) ,, ans
+  where
+    ans : polysEqual (map (λ z → z) ms) (map (λ z → z) ys)
+    ans rewrite mapId ms | mapId ys = Equivalence.transitive (Setoid.eq naivePolySetoid) snd snd2
++PwellDefined {m :: ms} {[]} {x :: xs} {[]} (fst ,, snd) n=y = fst ,, ans
+  where
+    ans : polysEqual (map (λ z → z) ms) (map (λ z → z) xs)
+    ans rewrite mapId ms | mapId xs = snd
++PwellDefined {m :: ms} {[]} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric identRight) (+WellDefined fst (symmetric fst2)) ,, identityOfIndiscernablesLeft polysEqual (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.symmetric (Setoid.eq naivePolySetoid) PidentRight) (+PwellDefined snd snd2)) (equalityCommutative (mapId ms))
++PwellDefined {m :: ms} {n :: ns} {[]} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identLeft ,, +PwellDefined snd snd2
++PwellDefined {m :: ms} {n :: ns} {[]} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identLeft ,, +PwellDefined snd snd2
++PwellDefined {m :: ms} {n :: ns} {x :: xs} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive (+WellDefined fst fst2) identRight ,, identityOfIndiscernablesRight polysEqual (Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined snd snd2) PidentRight) (equalityCommutative (mapId xs))
++PwellDefined {m :: ms} {n :: ns} {x :: xs} {y :: ys} (fst ,, snd) (fst2 ,, snd2) = +WellDefined fst fst2 ,, +PwellDefined snd snd2
+
+PidentLeft : {m : NaivePoly} → polysEqual ([] +P m) m
+PidentLeft {[]} = record {}
+PidentLeft {x :: m} = reflexive ,, identityOfIndiscernablesLeft polysEqual (Equivalence.reflexive (Setoid.eq naivePolySetoid)) (equalityCommutative (mapId m))
diff --git a/Groups/Polynomials/Definition.agda b/Groups/Polynomials/Definition.agda
new file mode 100644
index 0000000..6694035
--- /dev/null
+++ b/Groups/Polynomials/Definition.agda
@@ -0,0 +1,131 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Definition
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Vectors
+open import Lists.Lists
+open import Maybe
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Groups.Polynomials.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where
+
+open Setoid S
+open Equivalence eq
+open Group G
+
+NaivePoly : Set a
+NaivePoly = List A
+
+0P : NaivePoly
+0P = []
+
+polysEqual : NaivePoly → NaivePoly → Set (a ⊔ b)
+polysEqual [] [] = True'
+polysEqual [] (x :: b) = (x ∼ 0G) && polysEqual [] b
+polysEqual (x :: a) [] = (x ∼ 0G) && polysEqual a []
+polysEqual (x :: a) (y :: b) = (x ∼ y) && polysEqual a b
+
+polysReflexive : {x : NaivePoly} → polysEqual x x
+polysReflexive {[]} = record {}
+polysReflexive {x :: y} = reflexive ,, polysReflexive
+
+polysSymmetricZero : {x : NaivePoly} → polysEqual [] x → polysEqual x []
+polysSymmetricZero {[]} 0=x = record {}
+polysSymmetricZero {x :: y} (fst ,, snd) = fst ,, polysSymmetricZero snd
+
+polysSymmetricZero' : {x : NaivePoly} → polysEqual x [] → polysEqual [] x
+polysSymmetricZero' {[]} 0=x = record {}
+polysSymmetricZero' {x :: y} (fst ,, snd) = fst ,, polysSymmetricZero' snd
+
+polysSymmetric : {x y : NaivePoly} → polysEqual x y → polysEqual y x
+polysSymmetric {[]} {y} x=y = polysSymmetricZero x=y
+polysSymmetric {x :: xs} {[]} x=y = polysSymmetricZero' {x :: xs} x=y
+polysSymmetric {x :: xs} {y :: ys} (fst ,, snd) = symmetric fst ,, polysSymmetric {xs} {ys} snd
+
+polysTransitive : {x y z : NaivePoly} → polysEqual x y → polysEqual y z → polysEqual x z
+polysTransitive {[]} {[]} {[]} x=y y=z = record {}
+polysTransitive {[]} {[]} {x :: z} x=y y=z = y=z
+polysTransitive {[]} {x :: y} {[]} (fst ,, snd) y=z = record {}
+polysTransitive {[]} {x :: y} {x₁ :: z} (fst ,, snd) (fst2 ,, snd2) = transitive (symmetric fst2) fst ,, polysTransitive snd snd2
+polysTransitive {x :: xs} {[]} {[]} x=y y=z = x=y
+polysTransitive {x :: xs} {[]} {z :: zs} (fst ,, snd) (fst2 ,, snd2) = transitive fst (symmetric fst2) ,, polysTransitive snd snd2
+polysTransitive {x :: xs} {y :: ys} {[]} (fst ,, snd) (fst2 ,, snd2) = transitive fst fst2 ,, polysTransitive snd snd2
+polysTransitive {x :: xs} {y :: ys} {z :: zs} (fst ,, snd) (fst2 ,, snd2) = transitive fst fst2 ,, polysTransitive snd snd2
+
+naivePolySetoid : Setoid NaivePoly
+Setoid._∼_ naivePolySetoid = polysEqual
+Equivalence.reflexive (Setoid.eq naivePolySetoid) = polysReflexive
+Equivalence.symmetric (Setoid.eq naivePolySetoid) = polysSymmetric
+Equivalence.transitive (Setoid.eq naivePolySetoid) = polysTransitive
+
+polyInjection : A → NaivePoly
+polyInjection a = a :: []
+
+polyInjectionIsInj : SetoidInjection S naivePolySetoid polyInjection
+SetoidInjection.wellDefined polyInjectionIsInj x=y = x=y ,, record {}
+SetoidInjection.injective polyInjectionIsInj {x} {y} (fst ,, snd) = fst
+
+-- the zero polynomial has no degree
+-- all other polynomials have a degree
+
+degree : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False)) → NaivePoly → Maybe ℕ
+degree decide [] = no
+degree decide (x :: poly) with decide x
+degree decide (x :: poly) | inl x=0 with degree decide poly
+degree decide (x :: poly) | inl x=0 | no = no
+degree decide (x :: poly) | inl x=0 | yes deg = yes (succ deg)
+degree decide (x :: poly) | inr x!=0 with degree decide poly
+degree decide (x :: poly) | inr x!=0 | no = yes 0
+degree decide (x :: poly) | inr x!=0 | yes n = yes (succ n)
+
+degreeWellDefined : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) {x y : NaivePoly} → polysEqual x y → degree decide x ≡ degree decide y
+degreeWellDefined decide {[]} {[]} x=y = refl
+degreeWellDefined decide {[]} {x :: y} (fst ,, snd) with decide x
+degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 with inspect (degree decide y)
+degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
+degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inl x=0 | yes bad with≡ pr rewrite pr = exFalso (noNotYes (transitivity (degreeWellDefined decide {[]} {y} snd) pr))
+degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 with inspect (degree decide y)
+degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 | no with≡ pr rewrite pr = exFalso (x!=0 fst)
+degreeWellDefined decide {[]} {x :: y} (fst ,, snd) | inr x!=0 | yes deg with≡ pr rewrite pr = exFalso (x!=0 fst)
+degreeWellDefined decide {x :: xs} {[]} x=y with decide x
+degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 with inspect (degree decide xs)
+degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
+degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inl x=0 | yes bad with≡ pr rewrite pr = exFalso (noNotYes (transitivity (equalityCommutative (degreeWellDefined decide snd)) pr))
+degreeWellDefined decide {x :: xs} {[]} (fst ,, snd) | inr x!=0 = exFalso (x!=0 fst)
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) with decide x
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 with decide y
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 with inspect (degree decide ys)
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 | no with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inl y=0 | (yes th) with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inl x=0 | inr y!=0 = exFalso (y!=0 (transitive (symmetric fst) x=0))
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 with decide y
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inl y=0 = exFalso (x!=0 (transitive fst y=0))
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 with inspect (degree decide ys)
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 | no with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
+degreeWellDefined decide {x :: xs} {y :: ys} (fst ,, snd) | inr x!=0 | inr y!=0 | yes x₁ with≡ pr rewrite degreeWellDefined decide {xs} {ys} snd | pr = refl
+
+degreeNoImpliesZero : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) → (a : NaivePoly) → degree decide a ≡ no → polysEqual a []
+degreeNoImpliesZero decide [] not = record {}
+degreeNoImpliesZero decide (x :: a) not with decide x
+degreeNoImpliesZero decide (x :: a) not | inl x=0 with inspect (degree decide a)
+degreeNoImpliesZero decide (x :: a) not | inl x=0 | no with≡ pr rewrite pr = x=0 ,, degreeNoImpliesZero decide a pr
+degreeNoImpliesZero decide (x :: a) not | inl x=0 | (yes deg) with≡ pr rewrite pr = exFalso (noNotYes (equalityCommutative not))
+degreeNoImpliesZero decide (x :: a) not | inr x!=0 with degree decide a
+degreeNoImpliesZero decide (x :: a) () | inr x!=0 | no
+degreeNoImpliesZero decide (x :: a) () | inr x!=0 | yes x₁
+
+emptyImpliesDegreeZero : (decide : ((x : A) → (x ∼ 0G) || ((x ∼ 0G) → False))) → (a : NaivePoly) → polysEqual a [] → degree decide a ≡ no
+emptyImpliesDegreeZero decide [] a=[] = refl
+emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) with decide x
+emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 with inspect (degree decide a)
+emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 | no with≡ pr rewrite pr = refl
+emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inl x=0 | (yes deg) with≡ pr rewrite pr = exFalso (noNotYes (transitivity (equalityCommutative (emptyImpliesDegreeZero decide a snd)) pr))
+emptyImpliesDegreeZero decide (x :: a) (fst ,, snd) | inr x!=0 = exFalso (x!=0 fst)
diff --git a/Groups/Polynomials/Examples.agda b/Groups/Polynomials/Examples.agda
new file mode 100644
index 0000000..7a59c08
--- /dev/null
+++ b/Groups/Polynomials/Examples.agda
@@ -0,0 +1,35 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Definition
+open import Numbers.Integers.Integers
+open import Numbers.Integers.Definition
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Vectors
+open import Lists.Lists
+open import Maybe
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Groups.Polynomials.Examples where
+
+open import Groups.Polynomials.Definition ℤGroup
+
+private
+  decide : _
+  decide = (λ a → ℤDecideEquality a (nonneg 0))
+
+  p1 : degree decide [] ≡ no
+  p1 = refl
+
+  p2 : degree decide (nonneg 0 :: []) ≡ no
+  p2 = refl
+
+  p3 : degree decide (nonneg 1 :: []) ≡ yes 0
+  p3 = refl
diff --git a/Groups/Polynomials/Group.agda b/Groups/Polynomials/Group.agda
new file mode 100644
index 0000000..c4eb969
--- /dev/null
+++ b/Groups/Polynomials/Group.agda
@@ -0,0 +1,81 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Abelian.Definition
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Definition
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Vectors
+open import Lists.Lists
+open import Maybe
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Groups.Polynomials.Group {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) where
+
+open import Groups.Polynomials.Definition G
+open import Groups.Polynomials.Addition G public
+open Setoid S
+open Equivalence eq
+
+inverse : NaivePoly → NaivePoly
+inverse = map (Group.inverse G)
+
+invLeft : {a : NaivePoly} → polysEqual ((inverse a) +P a) []
+invLeft {[]} = record {}
+invLeft {x :: a} = Group.invLeft G ,, invLeft {a}
+
+invRight : {a : NaivePoly} → polysEqual (a +P (inverse a)) []
+invRight {[]} = record {}
+invRight {x :: a} = Group.invRight G ,, invRight {a}
+
+assoc : {a b c : NaivePoly} → polysEqual (a +P (b +P c)) ((a +P b) +P c)
+assoc {[]} {[]} {[]} = record {}
+assoc {[]} {[]} {x :: c} = reflexive ,, ans
+  where
+    ans : polysEqual (map (λ z → z) (map (λ z → z) c)) (map (λ z → z) c)
+    ans rewrite mapId c | mapId c = Equivalence.reflexive (Setoid.eq naivePolySetoid)
+assoc {[]} {b :: bs} {[]} = reflexive ,, ans
+  where
+    ans : polysEqual (map (λ z → z) (map (λ z → z) bs)) (map (λ z → z) (map (λ z → z) bs))
+    ans rewrite mapId bs | mapId bs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
+assoc {[]} {b :: bs} {c :: cs} = reflexive ,, ans
+  where
+    ans : polysEqual (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) bs cs)) (listZip _+_ (λ z → z) (λ z → z) (map (λ z → z) bs) cs)
+    ans rewrite mapId bs | mapId (listZip _+_ id id bs cs) = Equivalence.reflexive (Setoid.eq naivePolySetoid)
+assoc {a :: as} {[]} {[]} = reflexive ,, ans
+  where
+    ans : polysEqual (map (λ z → z) as) (map (λ z → z) (map (λ z → z) as))
+    ans rewrite mapId as | mapId as = Equivalence.reflexive (Setoid.eq naivePolySetoid)
+assoc {a :: as} {[]} {c :: cs} = reflexive ,, ans
+  where
+    ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) as (map (λ z → z) cs)) (listZip _+_ (λ z → z) (λ z → z) (map (λ z → z) as) cs)
+    ans rewrite mapId cs | mapId as = Equivalence.reflexive (Setoid.eq naivePolySetoid)
+assoc {a :: as} {b :: bs} {[]} = reflexive ,, ans
+  where
+    ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) as (map (λ z → z) bs)) (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) as bs))
+    ans rewrite mapId (listZip _+_ id id as bs) | mapId bs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
+assoc {a :: as} {b :: bs} {c :: cs} = Group.+Associative G ,, assoc {as} {bs} {cs}
+
+polyGroup : Group naivePolySetoid _+P_
+Group.+WellDefined polyGroup = +PwellDefined
+Group.0G polyGroup = []
+Group.inverse polyGroup = inverse
+Group.+Associative polyGroup {a} {b} {c} = assoc {a} {b} {c}
+Group.identRight polyGroup = PidentRight
+Group.identLeft polyGroup = PidentLeft
+Group.invLeft polyGroup {a} = invLeft {a}
+Group.invRight polyGroup {a} = invRight {a}
+
+comm : AbelianGroup G → {x y : NaivePoly} → polysEqual (x +P y) (y +P x)
+comm com {[]} {y} = Equivalence.transitive (Setoid.eq naivePolySetoid) (Group.identLeft polyGroup) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.identRight polyGroup))
+comm com {x :: xs} {[]} = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
+comm com {x :: xs} {y :: ys} = AbelianGroup.commutative com ,, comm com {xs} {ys}
+
+abelian : AbelianGroup G → AbelianGroup polyGroup
+AbelianGroup.commutative (abelian ab) {x} {y} = comm ab {x} {y}
diff --git a/Lists/Lists.agda b/Lists/Lists.agda
index 82152b5..cfe637c 100644
--- a/Lists/Lists.agda
+++ b/Lists/Lists.agda
@@ -5,155 +5,177 @@ open import Functions
 open import Numbers.Naturals.Semiring -- for length
 open import Numbers.Naturals.Order
 open import Semirings.Definition
+open import Maybe
 
 module Lists.Lists where
-  data List {a} (A : Set a) : Set a where
-    [] : List A
-    _::_ : (x : A) (xs : List A) → List A
-  infixr 10 _::_
 
-  [_] : {a : _} → {A : Set a} → (a : A) → List A
-  [ a ] = a :: []
+data List {a} (A : Set a) : Set a where
+  [] : List A
+  _::_ : (x : A) (xs : List A) → List A
+infixr 10 _::_
 
-  _++_ : {a : _} → {A : Set a} → List A → List A → List A
-  [] ++ m = m
-  (x :: l) ++ m = x :: (l ++ m)
+[_] : {a : _} → {A : Set a} → (a : A) → List A
+[ a ] = a :: []
 
-  appendEmptyList : {a : _} → {A : Set a} → (l : List A) → (l ++ [] ≡ l)
-  appendEmptyList [] = refl
-  appendEmptyList (x :: l) = applyEquality (_::_ x) (appendEmptyList l)
+_++_ : {a : _} → {A : Set a} → List A → List A → List A
+[] ++ m = m
+(x :: l) ++ m = x :: (l ++ m)
 
-  concatAssoc : {a : _} → {A : Set a} → (x : List A) → (y : List A) → (z : List A) → ((x ++ y) ++ z) ≡ x ++ (y ++ z)
-  concatAssoc [] m n = refl
-  concatAssoc (x :: l) m n = applyEquality (_::_ x) (concatAssoc l m n)
+appendEmptyList : {a : _} → {A : Set a} → (l : List A) → (l ++ [] ≡ l)
+appendEmptyList [] = refl
+appendEmptyList (x :: l) = applyEquality (_::_ x) (appendEmptyList l)
 
-  canMovePrepend : {a : _} → {A : Set a} → (l : A) → {m n : ℕ} → (x : List A) (y : List A) → ((l :: x) ++ y ≡ l :: (x ++ y))
-  canMovePrepend l [] n = refl
-  canMovePrepend l (x :: m) n = refl
+concatAssoc : {a : _} → {A : Set a} → (x : List A) → (y : List A) → (z : List A) → ((x ++ y) ++ z) ≡ x ++ (y ++ z)
+concatAssoc [] m n = refl
+concatAssoc (x :: l) m n = applyEquality (_::_ x) (concatAssoc l m n)
 
-  rev : {a : _} → {A : Set a} → List A → List A
-  rev [] = []
-  rev (x :: l) = (rev l) ++ [ x ]
+canMovePrepend : {a : _} → {A : Set a} → (l : A) → {m n : ℕ} → (x : List A) (y : List A) → ((l :: x) ++ y ≡ l :: (x ++ y))
+canMovePrepend l [] n = refl
+canMovePrepend l (x :: m) n = refl
 
-  revIsHom : {a : _} → {A : Set a} → (l1 : List A) → (l2 : List A) → (rev (l1 ++ l2) ≡ (rev l2) ++ (rev l1))
-  revIsHom l1 [] = applyEquality rev (appendEmptyList l1)
-  revIsHom [] (x :: l2) with (rev l2 ++ [ x ])
-  ... | r = equalityCommutative (appendEmptyList r)
-  revIsHom (w :: l1) (x :: l2) = transitivity t (equalityCommutative s)
-    where
-      s : ((rev l2 ++ [ x ]) ++ (rev l1 ++ [ w ])) ≡ (((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ])
-      s = equalityCommutative (concatAssoc (rev l2 ++ (x :: [])) (rev l1) ([ w ]))
-      t' : rev (l1 ++ (x :: l2)) ≡ rev (x :: l2) ++ rev l1
-      t' = revIsHom l1 (x :: l2)
-      t : (rev (l1 ++ (x :: l2)) ++ [ w ]) ≡ ((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ]
-      t = applyEquality (λ r → r ++ [ w ]) {rev (l1 ++ (x :: l2))} {((rev l2) ++ [ x ]) ++ rev l1} (transitivity t' (applyEquality (λ r → r ++ rev l1) {rev l2 ++ (x :: [])} {rev l2 ++ (x :: [])} refl))
+rev : {a : _} → {A : Set a} → List A → List A
+rev [] = []
+rev (x :: l) = (rev l) ++ [ x ]
 
-  revRevIsId : {a : _} → {A : Set a} → (l : List A) → (rev (rev l) ≡ l)
-  revRevIsId [] = refl
-  revRevIsId (x :: l) = t
-    where
-      s : rev (rev l ++ [ x ] ) ≡ [ x ] ++ rev (rev l)
-      s = revIsHom (rev l) [ x ]
-      t : rev (rev l ++ [ x ] ) ≡ [ x ] ++ l
-      t = identityOfIndiscernablesRight _≡_ s (applyEquality (λ n → [ x ] ++ n) (revRevIsId l))
+revIsHom : {a : _} → {A : Set a} → (l1 : List A) → (l2 : List A) → (rev (l1 ++ l2) ≡ (rev l2) ++ (rev l1))
+revIsHom l1 [] = applyEquality rev (appendEmptyList l1)
+revIsHom [] (x :: l2) with (rev l2 ++ [ x ])
+... | r = equalityCommutative (appendEmptyList r)
+revIsHom (w :: l1) (x :: l2) = transitivity t (equalityCommutative s)
+  where
+    s : ((rev l2 ++ [ x ]) ++ (rev l1 ++ [ w ])) ≡ (((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ])
+    s = equalityCommutative (concatAssoc (rev l2 ++ (x :: [])) (rev l1) ([ w ]))
+    t' : rev (l1 ++ (x :: l2)) ≡ rev (x :: l2) ++ rev l1
+    t' = revIsHom l1 (x :: l2)
+    t : (rev (l1 ++ (x :: l2)) ++ [ w ]) ≡ ((rev l2 ++ [ x ]) ++ rev l1) ++ [ w ]
+    t = applyEquality (λ r → r ++ [ w ]) {rev (l1 ++ (x :: l2))} {((rev l2) ++ [ x ]) ++ rev l1} (transitivity t' (applyEquality (λ r → r ++ rev l1) {rev l2 ++ (x :: [])} {rev l2 ++ (x :: [])} refl))
 
-  fold : {a b : _} {A : Set a} {B : Set b} (f : A → B → B) → B → List A → B
-  fold f default [] = default
-  fold f default (x :: l) = f x (fold f default l)
+revRevIsId : {a : _} → {A : Set a} → (l : List A) → (rev (rev l) ≡ l)
+revRevIsId [] = refl
+revRevIsId (x :: l) = t
+  where
+    s : rev (rev l ++ [ x ] ) ≡ [ x ] ++ rev (rev l)
+    s = revIsHom (rev l) [ x ]
+    t : rev (rev l ++ [ x ] ) ≡ [ x ] ++ l
+    t = identityOfIndiscernablesRight _≡_ s (applyEquality (λ n → [ x ] ++ n) (revRevIsId l))
 
-  map : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → List A → List B
-  map f [] = []
-  map f (x :: list) = (f x) :: (map f list)
+fold : {a b : _} {A : Set a} {B : Set b} (f : A → B → B) → B → List A → B
+fold f default [] = default
+fold f default (x :: l) = f x (fold f default l)
 
-  map' : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → List A → List B
-  map' f = fold (λ a → (f a) ::_ ) []
+map : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → List A → List B
+map f [] = []
+map f (x :: list) = (f x) :: (map f list)
 
-  map=map' : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → (l : List A) → (map f l ≡ map' f l)
-  map=map' f [] = refl
-  map=map' f (x :: l) with map=map' f l
-  ... | bl = applyEquality (f x ::_) bl
+map' : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → List A → List B
+map' f = fold (λ a → (f a) ::_ ) []
 
-  flatten : {a : _} {A : Set a} → (l : List (List A)) → List A
-  flatten [] = []
-  flatten (l :: ls) = l ++ flatten ls
+map=map' : {a : _} → {b : _} → {A : Set a} → {B : Set b} → (f : A → B) → (l : List A) → (map f l ≡ map' f l)
+map=map' f [] = refl
+map=map' f (x :: l) with map=map' f l
+... | bl = applyEquality (f x ::_) bl
 
-  flatten' : {a : _} {A : Set a} → (l : List (List A)) → List A
-  flatten' = fold _++_ []
+flatten : {a : _} {A : Set a} → (l : List (List A)) → List A
+flatten [] = []
+flatten (l :: ls) = l ++ flatten ls
 
-  flatten=flatten' : {a : _} {A : Set a} (l : List (List A)) → flatten l ≡ flatten' l
-  flatten=flatten' [] = refl
-  flatten=flatten' (l :: ls) = applyEquality (l ++_) (flatten=flatten' ls)
+flatten' : {a : _} {A : Set a} → (l : List (List A)) → List A
+flatten' = fold _++_ []
 
-  length : {a : _} {A : Set a} (l : List A) → ℕ
-  length [] = zero
-  length (x :: l) = succ (length l)
+flatten=flatten' : {a : _} {A : Set a} (l : List (List A)) → flatten l ≡ flatten' l
+flatten=flatten' [] = refl
+flatten=flatten' (l :: ls) = applyEquality (l ++_) (flatten=flatten' ls)
 
-  length' : {a : _} {A : Set a} → (l : List A) → ℕ
-  length' = fold (λ _ → succ) 0
+length : {a : _} {A : Set a} (l : List A) → ℕ
+length [] = zero
+length (x :: l) = succ (length l)
 
-  length=length' : {a : _} {A : Set a} (l : List A) → length l ≡ length' l
-  length=length' [] = refl
-  length=length' (x :: l) = applyEquality succ (length=length' l)
+length' : {a : _} {A : Set a} → (l : List A) → ℕ
+length' = fold (λ _ → succ) 0
 
-  total : List ℕ → ℕ
-  total [] = zero
-  total (x :: l) = x +N total l
+length=length' : {a : _} {A : Set a} (l : List A) → length l ≡ length' l
+length=length' [] = refl
+length=length' (x :: l) = applyEquality succ (length=length' l)
 
-  total' : List ℕ → ℕ
-  total' = fold _+N_ 0
+total : List ℕ → ℕ
+total [] = zero
+total (x :: l) = x +N total l
 
-  lengthConcat : {a : _} {A : Set a} (l1 l2 : List A) → length (l1 ++ l2) ≡ length l1 +N length l2
-  lengthConcat [] l2 = refl
-  lengthConcat (x :: l1) l2 = applyEquality succ (lengthConcat l1 l2)
+total' : List ℕ → ℕ
+total' = fold _+N_ 0
 
-  lengthFlatten : {a : _} {A : Set a} (l : List (List A)) → length (flatten l) ≡ total (map length l)
-  lengthFlatten [] = refl
-  lengthFlatten (l :: ls) rewrite lengthConcat l (flatten ls) | lengthFlatten ls = refl
+lengthConcat : {a : _} {A : Set a} (l1 l2 : List A) → length (l1 ++ l2) ≡ length l1 +N length l2
+lengthConcat [] l2 = refl
+lengthConcat (x :: l1) l2 = applyEquality succ (lengthConcat l1 l2)
 
-  lengthMap : {a b : _} {A : Set a} {B : Set b} → (l : List A) → {f : A → B} → length l ≡ length (map f l)
-  lengthMap [] {f} = refl
-  lengthMap (x :: l) {f} rewrite lengthMap l {f} = refl
+lengthFlatten : {a : _} {A : Set a} (l : List (List A)) → length (flatten l) ≡ total (map length l)
+lengthFlatten [] = refl
+lengthFlatten (l :: ls) rewrite lengthConcat l (flatten ls) | lengthFlatten ls = refl
 
-  mapMap : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (l : List A) → {f : A → B} {g : B → C} → map g (map f l) ≡ map (g ∘ f) l
-  mapMap [] = refl
-  mapMap (x :: l) {f = f} {g} rewrite mapMap l {f} {g} = refl
+lengthMap : {a b : _} {A : Set a} {B : Set b} → (l : List A) → {f : A → B} → length l ≡ length (map f l)
+lengthMap [] {f} = refl
+lengthMap (x :: l) {f} rewrite lengthMap l {f} = refl
 
-  mapExtension : {a b : _} {A : Set a} {B : Set b} (l : List A) (f g : A → B) → ({x : A} → (f x ≡ g x)) → map f l ≡ map g l
-  mapExtension [] f g pr = refl
-  mapExtension (x :: l) f g pr rewrite mapExtension l f g pr | pr {x} = refl
+mapMap : {a b c : _} {A : Set a} {B : Set b} {C : Set c} → (l : List A) → {f : A → B} {g : B → C} → map g (map f l) ≡ map (g ∘ f) l
+mapMap [] = refl
+mapMap (x :: l) {f = f} {g} rewrite mapMap l {f} {g} = refl
 
-  replicate : {a : _} {A : Set a} (n : ℕ) (x : A) → List A
-  replicate zero x = []
-  replicate (succ n) x = x :: replicate n x
+mapExtension : {a b : _} {A : Set a} {B : Set b} (l : List A) (f g : A → B) → ({x : A} → (f x ≡ g x)) → map f l ≡ map g l
+mapExtension [] f g pr = refl
+mapExtension (x :: l) f g pr rewrite mapExtension l f g pr | pr {x} = refl
 
-  allTrue : {a b : _} {A : Set a} (f : A → Set b) (l : List A) → Set b
-  allTrue f [] = True'
-  allTrue f (x :: l) = f x && allTrue f l
+replicate : {a : _} {A : Set a} (n : ℕ) (x : A) → List A
+replicate zero x = []
+replicate (succ n) x = x :: replicate n x
 
-  allTrueConcat : {a b : _} {A : Set a} (f : A → Set b) (l m : List A) → allTrue f l → allTrue f m → allTrue f (l ++ m)
-  allTrueConcat f [] m fl fm = fm
-  allTrueConcat f (x :: l) m (fst ,, snd) fm = fst ,, allTrueConcat f l m snd fm
+allTrue : {a b : _} {A : Set a} (f : A → Set b) (l : List A) → Set b
+allTrue f [] = True'
+allTrue f (x :: l) = f x && allTrue f l
 
-  allTrueFlatten : {a b : _} {A : Set a} (f : A → Set b) (l : List (List A)) → allTrue (λ i → allTrue f i) l → allTrue f (flatten l)
-  allTrueFlatten f [] pr = record {}
-  allTrueFlatten f ([] :: ls) pr = allTrueFlatten f ls (_&&_.snd pr)
-  allTrueFlatten f ((x :: l) :: ls) ((fx ,, fl) ,, snd) = fx ,, allTrueConcat f l (flatten ls) fl (allTrueFlatten f ls snd)
+allTrueConcat : {a b : _} {A : Set a} (f : A → Set b) (l m : List A) → allTrue f l → allTrue f m → allTrue f (l ++ m)
+allTrueConcat f [] m fl fm = fm
+allTrueConcat f (x :: l) m (fst ,, snd) fm = fst ,, allTrueConcat f l m snd fm
 
-  allTrueMap : {a b c : _} {A : Set a} {B : Set b} (pred : B → Set c) (f : A → B) (l : List A) → allTrue (pred ∘ f) l → allTrue pred (map f l)
-  allTrueMap pred f [] pr = record {}
-  allTrueMap pred f (x :: l) pr = _&&_.fst pr ,, allTrueMap pred f l (_&&_.snd pr)
+allTrueFlatten : {a b : _} {A : Set a} (f : A → Set b) (l : List (List A)) → allTrue (λ i → allTrue f i) l → allTrue f (flatten l)
+allTrueFlatten f [] pr = record {}
+allTrueFlatten f ([] :: ls) pr = allTrueFlatten f ls (_&&_.snd pr)
+allTrueFlatten f ((x :: l) :: ls) ((fx ,, fl) ,, snd) = fx ,, allTrueConcat f l (flatten ls) fl (allTrueFlatten f ls snd)
 
-  allTrueExtension : {a b : _} {A : Set a} (f g : A → Set b) (l : List A) → ({x : A} → f x → g x) → allTrue f l → allTrue g l
-  allTrueExtension f g [] pred t = record {}
-  allTrueExtension f g (x :: l) pred (fg ,, snd) = pred {x} fg ,, allTrueExtension f g l pred snd
+allTrueMap : {a b c : _} {A : Set a} {B : Set b} (pred : B → Set c) (f : A → B) (l : List A) → allTrue (pred ∘ f) l → allTrue pred (map f l)
+allTrueMap pred f [] pr = record {}
+allTrueMap pred f (x :: l) pr = _&&_.fst pr ,, allTrueMap pred f l (_&&_.snd pr)
 
-  allTrueTail : {a b : _} {A : Set a} (pred : A → Set b) (x : A) (l : List A) → allTrue pred (x :: l) → allTrue pred l
-  allTrueTail pred x l (fst ,, snd) = snd
+allTrueExtension : {a b : _} {A : Set a} (f g : A → Set b) (l : List A) → ({x : A} → f x → g x) → allTrue f l → allTrue g l
+allTrueExtension f g [] pred t = record {}
+allTrueExtension f g (x :: l) pred (fg ,, snd) = pred {x} fg ,, allTrueExtension f g l pred snd
 
-  head : {a : _} {A : Set a} (l : List A) (pr : 0 <N length l) → A
-  head [] (le x ())
-  head (x :: l) pr = x
+allTrueTail : {a b : _} {A : Set a} (pred : A → Set b) (x : A) (l : List A) → allTrue pred (x :: l) → allTrue pred l
+allTrueTail pred x l (fst ,, snd) = snd
 
-  lengthRev : {a : _} {A : Set a} (l : List A) → length (rev l) ≡ length l
-  lengthRev [] = refl
-  lengthRev (x :: l) rewrite lengthConcat (rev l) (x :: []) | lengthRev l | Semiring.commutative ℕSemiring (length l) 1 = refl
+head : {a : _} {A : Set a} (l : List A) (pr : 0 <N length l) → A
+head [] (le x ())
+head (x :: l) pr = x
+
+lengthRev : {a : _} {A : Set a} (l : List A) → length (rev l) ≡ length l
+lengthRev [] = refl
+lengthRev (x :: l) rewrite lengthConcat (rev l) (x :: []) | lengthRev l | Semiring.commutative ℕSemiring (length l) 1 = refl
+
+filter : {a : _} {A : Set a} (l : List A) (f : A → Bool) → List A
+filter [] f = []
+filter (x :: l) f with f x
+filter (x :: l) f | BoolTrue = x :: filter l f
+filter (x :: l) f | BoolFalse = filter l f
+
+listLast : {a : _} {A : Set a} (l : List A) → Maybe A
+listLast [] = no
+listLast (x :: []) = yes x
+listLast (x :: y :: l) = listLast (y :: l)
+
+listZip : {a b c : _} {A : Set a} {B : Set b} {C : Set c} (f : A → B → C) → (f1 : A → C) → (f2 : B → C) →(l1 : List A) (l2 : List B) → List C
+listZip f f1 f2 [] l2 = map f2 l2
+listZip f f1 f2 (x :: l1) [] = map f1 (x :: l1)
+listZip f f1 f2 (x :: l1) (y :: l2) = (f x y) :: listZip f f1 f2 l1 l2
+
+mapId : {a : _} {A : Set a} (l : List A) → map id l ≡ l
+mapId [] = refl
+mapId (x :: l) rewrite mapId l = refl
diff --git a/Numbers/Integers/Definition.agda b/Numbers/Integers/Definition.agda
index 0149828..5588f8d 100644
--- a/Numbers/Integers/Definition.agda
+++ b/Numbers/Integers/Definition.agda
@@ -8,3 +8,19 @@ module Numbers.Integers.Definition where
 data ℤ : Set where
   nonneg : ℕ → ℤ
   negSucc : ℕ → ℤ
+
+nonnegInjective : {a b : ℕ} → nonneg a ≡ nonneg b → a ≡ b
+nonnegInjective refl = refl
+
+negSuccInjective : {a b : ℕ} → negSucc a ≡ negSucc b → a ≡ b
+negSuccInjective refl = refl
+
+ℤDecideEquality : (a b : ℤ) → ((a ≡ b) || ((a ≡ b) → False))
+ℤDecideEquality (nonneg x) (nonneg y) with ℕDecideEquality x y
+ℤDecideEquality (nonneg x) (nonneg y) | inl eq = inl (applyEquality nonneg eq)
+ℤDecideEquality (nonneg x) (nonneg y) | inr non = inr λ i → non (nonnegInjective i)
+ℤDecideEquality (nonneg x) (negSucc y) = inr λ ()
+ℤDecideEquality (negSucc x) (nonneg x₁) = inr λ ()
+ℤDecideEquality (negSucc x) (negSucc y) with ℕDecideEquality x y
+ℤDecideEquality (negSucc x) (negSucc y) | inl eq = inl (applyEquality negSucc eq)
+ℤDecideEquality (negSucc x) (negSucc y) | inr non = inr λ i → non (negSuccInjective i)
diff --git a/Numbers/Integers/Integers.agda b/Numbers/Integers/Integers.agda
index 37eac41..bda1730 100644
--- a/Numbers/Integers/Integers.agda
+++ b/Numbers/Integers/Integers.agda
@@ -11,7 +11,9 @@ module Numbers.Integers.Integers where
 
 open Numbers.Integers.Definition using (ℤ ; nonneg ; negSucc) public
 open Numbers.Integers.Addition using (_+Z_ ; ℤGroup ; ℤAbGrp) public
-open Numbers.Integers.Multiplication using (_*Z_ ; ℤIntDom ; ℤRing) public
+open Numbers.Integers.Multiplication using (_*Z_) public
+open import Numbers.Integers.RingStructure.IntegralDomain public using (ℤIntDom) public
+open import Numbers.Integers.RingStructure.Ring public using (ℤRing) public
 open Numbers.Integers.Order using (_<Z_ ; ℤOrderedRing) public
 
 _-Z_ : ℤ → ℤ → ℤ
diff --git a/Numbers/Integers/Multiplication.agda b/Numbers/Integers/Multiplication.agda
index 3057496..a835dbb 100644
--- a/Numbers/Integers/Multiplication.agda
+++ b/Numbers/Integers/Multiplication.agda
@@ -24,176 +24,3 @@ negSucc x *Z negSucc y = nonneg ((succ x) *N (succ y))
 
 *ZInherits : (a b : ℕ) → nonneg (a *N b) ≡ (nonneg a) *Z (nonneg b)
 *ZInherits a b = refl
-
-*ZCommutative : (a b : ℤ) → a *Z b ≡ b *Z a
-*ZCommutative (nonneg x) (nonneg y) = applyEquality nonneg (multiplicationNIsCommutative x y)
-*ZCommutative (nonneg zero) (negSucc y) = refl
-*ZCommutative (nonneg (succ x)) (negSucc y) = refl
-*ZCommutative (negSucc x) (nonneg zero) = refl
-*ZCommutative (negSucc x) (nonneg (succ y)) = refl
-*ZCommutative (negSucc x) (negSucc y) = applyEquality nonneg (multiplicationNIsCommutative (succ x) (succ y))
-
-*ZleftIdent : (a : ℤ) → (nonneg 1) *Z a ≡ a
-*ZleftIdent (nonneg x) = applyEquality nonneg (Semiring.commutative ℕSemiring x 0)
-*ZleftIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
-
-*ZrightIdent : (a : ℤ) → a *Z (nonneg 1) ≡ a
-*ZrightIdent (nonneg x) = applyEquality nonneg (Semiring.productOneRight ℕSemiring x)
-*ZrightIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
-
-*ZZeroLeft : (a : ℤ) → nonneg 0 *Z a ≡ nonneg 0
-*ZZeroLeft (nonneg x) = refl
-*ZZeroLeft (negSucc x) = refl
-
-*ZZeroRight : (a : ℤ) → a *Z nonneg 0 ≡ nonneg 0
-*ZZeroRight (nonneg x) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring x)
-*ZZeroRight (negSucc x) = refl
-
-*ZAssociative : (a b c : ℤ) → a *Z (b *Z c) ≡ (a *Z b) *Z c
-*ZAssociative (nonneg zero) b c = transitivity (*ZZeroLeft (b *Z c)) (transitivity (equalityCommutative (*ZZeroLeft c)) (applyEquality (_*Z c) (equalityCommutative (*ZZeroLeft b))))
-*ZAssociative (nonneg (succ a)) (nonneg zero) c rewrite Semiring.productZeroRight ℕSemiring a | *ZZeroLeft c | Semiring.productZeroRight ℕSemiring a = refl
-*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring b | Semiring.productZeroRight ℕSemiring (b +N a *N succ b) | Semiring.productZeroRight ℕSemiring a = refl
-*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg (succ c)) = applyEquality nonneg (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
-*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc x) rewrite productDistributes' b (a *N succ b) x | Semiring.+Associative ℕSemiring x (b *N x) ((a *N succ b) *N x) | equalityCommutative (Semiring.+Associative ℕSemiring ((x +N b *N x) +N b) (a *N ((x +N b *N x) +N b)) a) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) ((a *N succ b) *N x) (b +N a *N succ b)) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) b (a *N ((x +N b *N x) +N b) +N a)) = applyEquality (λ i → negSucc ((x +N b *N x) +N i)) ans
-  where
-    ans3 : (succ b +N (succ b *N x)) *N a ≡ succ x *N (a *N succ b)
-    ans3 rewrite multiplicationNIsCommutative (succ b) x = transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a))
-    ans2 : a *N ((x +N b *N x) +N b) +N a ≡ (a *N succ b) +N (a *N succ b) *N x
-    ans2 rewrite multiplicationNIsCommutative (a *N succ b) x | Semiring.commutative ℕSemiring (succ b *N x) b | multiplicationNIsCommutative a (b +N (succ b *N x)) | Semiring.commutative ℕSemiring ((b +N (succ b *N x)) *N a) a = ans3
-    ans : b +N (a *N ((x +N b *N x) +N b) +N a) ≡ (a *N succ b) *N x +N (b +N a *N succ b)
-    ans rewrite Semiring.commutative ℕSemiring ((a *N succ b) *N x) (b +N a *N succ b) | equalityCommutative (Semiring.+Associative ℕSemiring b (a *N succ b) ((a *N succ b) *N x)) = applyEquality (b +N_) ans2
-*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg zero) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring a)
-*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg (succ c)) = applyEquality negSucc ans
-  where
-    ans4 : (b +N b *N c) +N (a *N b +N (a *N b) *N c) ≡ (b +N a *N b) +N (b *N c +N (a *N b) *N c)
-    ans4 rewrite Semiring.+Associative ℕSemiring (b +N b *N c) (a *N b) ((a *N b) *N c) | Semiring.+Associative ℕSemiring (b +N a *N b) (b *N c) ((a *N b) *N c) = applyEquality (_+N (a *N b) *N c) (transitivity (transitivity (applyEquality (_+N a *N b) (Semiring.commutative ℕSemiring b (b *N c))) (equalityCommutative (Semiring.+Associative ℕSemiring (b *N c) b (a *N b)))) (Semiring.commutative ℕSemiring (b *N c) (b +N a *N b)))
-    ans3 : ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) +N ((c +N a *N c) +N a) ≡ ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) +N ((a +N a *N c) +N c)
-    ans3 rewrite Semiring.commutative ℕSemiring (c +N a *N c) a | Semiring.commutative ℕSemiring c (a *N c) | Semiring.+Associative ℕSemiring a (a *N c) c = applyEquality (λ i → i +N ((a +N a *N c) +N c)) {(b +N b *N c) +N (a *N b +N (a *N b) *N c)} {(b +N a *N b) +N (b *N c +N (a *N b) *N c)} ans4
-    ans2 : (((b +N c *N b) +N (a *N b +N a *N (c *N b))) +N (c +N a *N c)) +N a ≡ (((b +N a *N b) +N (c *N b +N c *N (a *N b))) +N (a +N c *N a)) +N c
-    ans2 rewrite multiplicationNIsCommutative c b | multiplicationNIsCommutative c (a *N b) | Semiring.*Associative ℕSemiring a b c | multiplicationNIsCommutative c a = transitivity (equalityCommutative (Semiring.+Associative ℕSemiring ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) (c +N a *N c) a)) (transitivity ans3 (Semiring.+Associative ℕSemiring ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) (a +N a *N c) c))
-    ans : succ a *N ((succ c *N b) +N c) +N a ≡ succ c *N ((succ a *N b) +N a) +N c
-    ans = transitivity (applyEquality (_+N a) (productDistributes (succ a) (succ c *N b) c)) (transitivity (transitivity (applyEquality (λ i → ((((b +N c *N b) +N i) +N (c +N a *N c)) +N a)) (productDistributes a b (c *N b))) (transitivity ans2 (applyEquality (λ i → (((b +N a *N b) +N i) +N (a +N c *N a)) +N c) (equalityCommutative (productDistributes c b (a *N b)))))) (applyEquality (_+N c) (equalityCommutative (productDistributes (succ c) (succ a *N b) a))))
-*ZAssociative (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality nonneg ans
-  where
-    ans : succ a *N (succ b *N succ x) ≡ succ ((succ a *N b) +N a) *N succ x
-    ans rewrite Semiring.commutative ℕSemiring (succ a *N b) a | multiplicationNIsCommutative (succ a) b = transitivity (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)) (applyEquality (_*N succ x) {succ a *N succ b} {succ b *N succ a} (multiplicationNIsCommutative (succ a) (succ b)))
-*ZAssociative (negSucc a) (nonneg zero) c rewrite *ZZeroLeft c = refl
-*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite multiplicationNIsCommutative b 0 = refl
-*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc ans
-  where
-    ans2 : (d : ℕ) → ((succ b *N d) *N a) +N b *N d ≡ d *N ((succ b *N a) +N b)
-    ans2 d = transitivity (transitivity (applyEquality (((d +N b *N d) *N a) +N_) (multiplicationNIsCommutative b d)) (applyEquality (_+N d *N b) (transitivity (applyEquality (_*N a) {d +N b *N d} {d *N succ b} (multiplicationNIsCommutative (succ b) d)) (equalityCommutative (Semiring.*Associative ℕSemiring d (succ b) a))))) (equalityCommutative (Semiring.+DistributesOver* ℕSemiring d (succ b *N a) b))
-    ans : (succ (c +N b *N succ c) *N a) +N (c +N b *N succ c) ≡ (succ c *N ((succ b *N a) +N b)) +N c
-    ans rewrite Semiring.commutative ℕSemiring c (b *N succ c) | Semiring.+Associative ℕSemiring (succ (b *N succ c +N c) *N a) (b *N succ c) c | Semiring.commutative ℕSemiring (b *N succ c) c = applyEquality (_+N c) (ans2 (succ c))
-*ZAssociative (negSucc a) (nonneg (succ b)) (negSucc c) = applyEquality nonneg ans
-  where
-    ans : succ a *N ((succ ((succ b) *N c)) +N b) ≡ (succ (succ b *N a) +N b) *N succ c
-    ans rewrite Semiring.commutative ℕSemiring (succ b *N a) b | multiplicationNIsCommutative (succ b) a = transitivity (applyEquality (succ a *N_) (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring c (b *N c) b)) (applyEquality (c +N_) (transitivity (transitivity (Semiring.commutative ℕSemiring (b *N c) b) (applyEquality (b +N_) (multiplicationNIsCommutative b c))) (multiplicationNIsCommutative (succ c) b)))))) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
-*ZAssociative (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring (b +N a *N succ b) = refl
-*ZAssociative (negSucc a) (negSucc b) (nonneg (succ x)) = applyEquality nonneg (transitivity (applyEquality (succ a *N_) ans) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)))
-  where
-    ans : succ ((succ x *N b) +N x) ≡ (succ b *N succ x)
-    ans rewrite Semiring.commutative ℕSemiring (succ x *N b) x | multiplicationNIsCommutative (succ x) b = refl
-*ZAssociative (negSucc a) (negSucc b) (negSucc x) = applyEquality negSucc t
-  where
-    l1 : (a b c d e f g : ℕ) → (a +N b) +N d ≡ e +N (f +N g) → (a +N b) +N (c +N d) ≡ (c +N e) +N (f +N g)
-    l1 a b c d e f g pr rewrite Semiring.commutative ℕSemiring c d | Semiring.+Associative ℕSemiring (a +N b) d c | pr | Semiring.commutative ℕSemiring (e +N (f +N g)) c | Semiring.+Associative ℕSemiring c e (f +N g) = refl
-    v : (((succ b) *N succ x) *N a) ≡ (succ x) *N (a *N succ b)
-    v = transitivity (applyEquality (_*N a) (multiplicationNIsCommutative (succ b) (succ x))) (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a)))
-    u : (a +N (x +N b *N succ x) *N a) +N b *N succ x ≡ (b +N a *N succ b) *N x +N (b +N a *N succ b)
-    u = transitivity (transitivity (transitivity (Semiring.commutative ℕSemiring (a +N (x +N b *N succ x) *N a) (b *N succ x)) (transitivity (applyEquality (_+N (a +N (x +N b *N succ x) *N a)) (multiplicationNIsCommutative b (succ x))) (transitivity (applyEquality ((b +N x *N b) +N_) v) (equalityCommutative (productDistributes (succ x) b (a *N succ b)))))) (applyEquality ((b +N a *N succ b) +N_) (multiplicationNIsCommutative x (b +N a *N succ b)))) (Semiring.commutative ℕSemiring (b +N a *N succ b) ((b +N a *N succ b) *N x))
-    t : (a +N (x +N b *N succ x) *N a) +N (x +N b *N succ x) ≡ (x +N (b +N a *N succ b) *N x) +N (b +N a *N succ b)
-    t = l1 a ((x +N b *N succ x) *N a) x (b *N succ x) ((b +N (a *N succ b)) *N x) b (a *N succ b) u
-
-multLemma : (a b : ℕ) → a *N succ b ≡ a *N b +N a
-multLemma a b rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative a b = refl
-
-negSucc+Nonneg : (a b : ℕ) → negSucc a ≡ negSucc (a +N b) +Z nonneg b
-negSucc+Nonneg zero zero = refl
-negSucc+Nonneg zero (succ b) = negSucc+Nonneg zero b
-negSucc+Nonneg (succ a) zero rewrite Semiring.commutative ℕSemiring a 0 = refl
-negSucc+Nonneg (succ a) (succ b) rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring b a = negSucc+Nonneg (succ a) b
-
-distLemma : (a b : ℕ) →  negSucc a *Z nonneg b ≡ negSucc ((a +N b *N a) +N b) +Z nonneg (succ a)
-distLemma a b rewrite Semiring.commutative ℕSemiring (a +N b *N a) b | Semiring.commutative ℕSemiring a (b *N a) | Semiring.+Associative ℕSemiring b (b *N a) a = transitivity u (transitivity (equalityCommutative (+ZAssociative (negSucc ((b +N b *N a) +N a)) (nonneg a) (nonneg 1))) (applyEquality ((negSucc ((b +N b *N a) +N a)) +Z_) {nonneg a +Z nonneg 1} {nonneg (succ a)} (+ZCommutative (nonneg a) (nonneg 1))))
-  where
-    v : (a b : ℕ) → negSucc a *Z nonneg b ≡ (negSucc (b +N b *N a)) +Z nonneg 1
-    v zero zero = refl
-    v zero (succ b) rewrite Semiring.productZeroRight ℕSemiring b = applyEquality negSucc (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))
-    v (succ a) zero = refl
-    v (succ a) (succ b) = applyEquality negSucc (Semiring.commutative ℕSemiring (succ (a +N b *N succ a)) b)
-    u : negSucc a *Z nonneg b ≡ (negSucc ((b +N b *N a) +N a) +Z nonneg a) +Z nonneg 1
-    u = transitivity (v a b) (applyEquality (_+Z nonneg 1) (negSucc+Nonneg (b +N b *N a) a))
-
-*ZDistributesOver+Z : (a b c : ℤ) → a *Z (b +Z c) ≡ (a *Z b) +Z (a *Z c)
-*ZDistributesOver+Z (nonneg zero) b c rewrite *ZZeroLeft (b +Z c) | *ZZeroLeft b | *ZZeroLeft c = refl
-*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (nonneg c) rewrite Semiring.productZeroRight ℕSemiring a = refl
-*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (nonneg c) = applyEquality nonneg (productDistributes (succ a) (succ b) c)
-*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (negSucc c) rewrite Semiring.productZeroRight ℕSemiring a = refl
-*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productZeroRight ℕSemiring a = t a
-  where
-    t : (a : ℕ) → nonneg (succ a *N b) ≡ nonneg (succ a *N succ b) +Z negSucc a
-    t zero = refl
-    t (succ a) = transitivity (+Zinherits b (b +N a *N b)) (transitivity (applyEquality (nonneg b +Z_) (t a)) (transitivity (+ZAssociative (nonneg b) (nonneg (succ (b +N a *N succ b))) (negSucc a)) (applyEquality (_+Z negSucc a) {nonneg b +Z nonneg (succ (b +N a *N succ b))} {nonneg (b +N succ (b +N a *N succ b))} (equalityCommutative (+Zinherits b _)))))
-*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ x)) (negSucc (succ b)) = transitivity (applyEquality ((nonneg (succ a)) *Z_) (+ZCommutative (nonneg x) (negSucc b))) (transitivity (transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t) (+ZCommutative (negSucc ((b +N a *N succ b) +N a)) (nonneg (x +N a *N succ x))))
-  where
-    t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
-    t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
-*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring a = refl
-*ZDistributesOver+Z (nonneg (succ a)) (negSucc zero) (nonneg (succ x)) rewrite Semiring.productZeroRight ℕSemiring a = t a x
-  where
-    t : (a x : ℕ) → nonneg (succ a *N x) ≡ negSucc a +Z nonneg (succ a *N succ x)
-    t zero x = refl
-    t (succ a) x with t a x
-    ... | bl rewrite +Zinherits x (a *N x) | +Zinherits x (x +N a *N x) = transitivity (transitivity (applyEquality (nonneg x +Z_) (+Zinherits x (a *N x))) (+ZCommutative (nonneg x) (nonneg x +Z nonneg (a *N x)))) (transitivity (applyEquality (_+Z nonneg x) bl) (transitivity (equalityCommutative (+ZAssociative (negSucc a) (nonneg (succ x +N a *N succ x)) (nonneg x))) (applyEquality (λ i → negSucc a +Z nonneg i) {succ (x +N a *N succ x) +N x} {x +N succ (x +N a *N succ x)} (Semiring.commutative ℕSemiring (succ (x +N a *N succ x)) x))))
-*ZDistributesOver+Z (nonneg (succ a)) (negSucc (succ b)) (nonneg (succ x)) = transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t
-  where
-    t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
-    t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
-*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality negSucc (transitivity (applyEquality (_+N a) (transitivity (productDistributes (succ a) (succ b) x) (applyEquality (_+N (x +N a *N x)) {succ b +N a *N succ b} {succ (b +N a *N b) +N a} (applyEquality succ u)))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ ((b +N a *N b) +N a)) (succ a *N x) a)))
-  where
-    u : b +N a *N succ b ≡ (succ a *N b) +N a
-    u rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative b a = Semiring.+Associative ℕSemiring b (a *N b) a
-*ZDistributesOver+Z (negSucc a) (nonneg zero) (nonneg x) = refl
-*ZDistributesOver+Z (negSucc a) (nonneg zero) (negSucc x) = refl
-*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite Semiring.commutative ℕSemiring b 0 = refl
-*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc t
-  where
-    v : a *N b +N a *N succ c ≡ c *N a +N (a +N b *N a)
-    v rewrite multiplicationNIsCommutative b a | Semiring.+Associative ℕSemiring (c *N a) a (a *N b) | Semiring.commutative ℕSemiring (c *N a +N a) (a *N b) | Semiring.commutative ℕSemiring (c *N a) a = applyEquality (λ i → a *N b +N i) (transitivity (multLemma a c) (transitivity (Semiring.commutative ℕSemiring (a *N c) a) (applyEquality (a +N_) (multiplicationNIsCommutative a c))))
-    u : (a +N (b +N succ c) *N a) +N b ≡ (a +N c *N a) +N ((a +N b *N a) +N b)
-    u rewrite Semiring.+Associative ℕSemiring (a +N c *N a) (a +N b *N a) b | (equalityCommutative (Semiring.+Associative ℕSemiring a (c *N a) (a +N b *N a))) = applyEquality (λ i → (a +N i) +N b) (transitivity (multiplicationNIsCommutative (b +N succ c) a) (transitivity (productDistributes a b (succ c)) v))
-    t : (a +N (b +N succ c) *N a) +N (b +N succ c) ≡ succ (((a +N b *N a) +N b) +N ((a +N c *N a) +N c))
-    t rewrite Semiring.+Associative ℕSemiring ((a +N (b +N succ c) *N a)) b (succ c) | Semiring.commutative ℕSemiring ((a +N b *N a) +N b) ((a +N c *N a) +N c) | Semiring.commutative ℕSemiring (a +N c *N a) c | equalityCommutative (Semiring.+Associative ℕSemiring (succ c) (a +N c *N a) ((a +N b *N a) +N b)) | Semiring.commutative ℕSemiring (succ c) ((a +N c *N a) +N ((a +N b *N a) +N b)) = applyEquality (_+N succ c) u
-*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productOneRight ℕSemiring a = distLemma a b
-*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc (succ c)) = transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))
-  where
-    t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
-    t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
-*ZDistributesOver+Z (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.commutative ℕSemiring (b +N a *N succ b) 0 = refl
-*ZDistributesOver+Z (negSucc a) (negSucc zero) (nonneg (succ b)) = transitivity (distLemma a b) (transitivity (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a))) (applyEquality (λ i → nonneg (succ i) +Z negSucc ((a +N b *N a) +N b)) (equalityCommutative (Semiring.productOneRight ℕSemiring a))))
-*ZDistributesOver+Z (negSucc a) (negSucc (succ c)) (nonneg (succ b)) = transitivity (applyEquality (negSucc a *Z_) (+ZCommutative (negSucc c) (nonneg b))) (transitivity (transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))) (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ (succ (c +N a *N succ (succ c)))))))
-  where
-    t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
-    t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
-*ZDistributesOver+Z (negSucc a) (negSucc b) (negSucc c) = applyEquality nonneg (transitivity (applyEquality (λ i → succ a *N (succ i)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring b c)) (Semiring.commutative ℕSemiring (succ c) b))) (productDistributes (succ a) (succ b) (succ c)))
-
-ℤRing : Ring (reflSetoid ℤ) _+Z_ _*Z_
-Ring.additiveGroup ℤRing = ℤGroup
-Ring.*WellDefined ℤRing refl refl = refl
-Ring.1R ℤRing = nonneg 1
-Ring.groupIsAbelian ℤRing {a} {b} = +ZCommutative a b
-Ring.*Associative ℤRing {a} {b} {c} = *ZAssociative a b c
-Ring.*Commutative ℤRing {a} {b} = *ZCommutative a b
-Ring.*DistributesOver+ ℤRing {a} {b} {c} = *ZDistributesOver+Z a b c
-Ring.identIsIdent ℤRing {a} = *ZleftIdent a
-
-intDom : (a b : ℤ) → a *Z b ≡ nonneg 0 → (a ≡ nonneg 0) || (b ≡ nonneg 0)
-intDom (nonneg zero) (nonneg b) pr = inl refl
-intDom (nonneg (succ a)) (nonneg zero) pr = inr refl
-intDom (nonneg zero) (negSucc b) pr = inl refl
-intDom (negSucc a) (nonneg zero) pr = inr refl
-
-ℤIntDom : IntegralDomain ℤRing
-IntegralDomain.intDom ℤIntDom {a} {b} = intDom a b
-IntegralDomain.nontrivial ℤIntDom ()
diff --git a/Numbers/Integers/Order.agda b/Numbers/Integers/Order.agda
index 880c631..536ee60 100644
--- a/Numbers/Integers/Order.agda
+++ b/Numbers/Integers/Order.agda
@@ -4,6 +4,7 @@ open import LogicalFormulae
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Numbers.Integers.Definition
+open import Numbers.Integers.RingStructure.Ring
 open import Numbers.Integers.Addition
 open import Numbers.Integers.Multiplication
 open import Semirings.Definition
@@ -30,9 +31,6 @@ lessLemma (succ a) x pr = lessLemma a x q
     q : succ x +N a ≡ a
     q rewrite Semiring.commutative ℕSemiring a (succ x) | Semiring.commutative ℕSemiring x a | Semiring.commutative ℕSemiring (succ a) x = succInjective pr
 
-nonnegInjective : {a b : ℕ} → (nonneg a ≡ nonneg b) → (a ≡ b)
-nonnegInjective {a} {.a} refl = refl
-
 irreflexive : (x : ℤ) → x <Z x → False
 irreflexive (nonneg x) record { x = y ; proof = proof } = lessLemma x y (nonnegInjective proof)
 irreflexive (negSucc a) record { x = x ; proof = proof } = naughtE (equalityCommutative q)
diff --git a/Numbers/Integers/RingStructure/IntegralDomain.agda b/Numbers/Integers/RingStructure/IntegralDomain.agda
new file mode 100644
index 0000000..e1637d0
--- /dev/null
+++ b/Numbers/Integers/RingStructure/IntegralDomain.agda
@@ -0,0 +1,23 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Multiplication
+open import Numbers.Integers.RingStructure.Ring
+open import Semirings.Definition
+open import Groups.Definition
+open import Rings.Definition
+open import Setoids.Setoids
+open import Rings.IntegralDomains
+
+module Numbers.Integers.RingStructure.IntegralDomain where
+
+intDom : (a b : ℤ) → a *Z b ≡ nonneg 0 → (a ≡ nonneg 0) || (b ≡ nonneg 0)
+intDom (nonneg zero) (nonneg b) pr = inl refl
+intDom (nonneg (succ a)) (nonneg zero) pr = inr refl
+intDom (nonneg zero) (negSucc b) pr = inl refl
+intDom (negSucc a) (nonneg zero) pr = inr refl
+
+ℤIntDom : IntegralDomain ℤRing
+IntegralDomain.intDom ℤIntDom {a} {b} = intDom a b
+IntegralDomain.nontrivial ℤIntDom ()
diff --git a/Numbers/Integers/RingStructure/Ring.agda b/Numbers/Integers/RingStructure/Ring.agda
new file mode 100644
index 0000000..b490855
--- /dev/null
+++ b/Numbers/Integers/RingStructure/Ring.agda
@@ -0,0 +1,179 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Multiplication
+open import Semirings.Definition
+open import Groups.Definition
+open import Rings.Definition
+open import Setoids.Setoids
+open import Rings.IntegralDomains
+
+module Numbers.Integers.RingStructure.Ring where
+
+open import Numbers.Integers.Definition public
+open import Numbers.Integers.Addition public
+open import Numbers.Integers.Multiplication public
+
+*ZCommutative : (a b : ℤ) → a *Z b ≡ b *Z a
+*ZCommutative (nonneg x) (nonneg y) = applyEquality nonneg (multiplicationNIsCommutative x y)
+*ZCommutative (nonneg zero) (negSucc y) = refl
+*ZCommutative (nonneg (succ x)) (negSucc y) = refl
+*ZCommutative (negSucc x) (nonneg zero) = refl
+*ZCommutative (negSucc x) (nonneg (succ y)) = refl
+*ZCommutative (negSucc x) (negSucc y) = applyEquality nonneg (multiplicationNIsCommutative (succ x) (succ y))
+
+*ZleftIdent : (a : ℤ) → (nonneg 1) *Z a ≡ a
+*ZleftIdent (nonneg x) = applyEquality nonneg (Semiring.commutative ℕSemiring x 0)
+*ZleftIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
+
+*ZrightIdent : (a : ℤ) → a *Z (nonneg 1) ≡ a
+*ZrightIdent (nonneg x) = applyEquality nonneg (Semiring.productOneRight ℕSemiring x)
+*ZrightIdent (negSucc x) = applyEquality negSucc (transitivity (Semiring.commutative ℕSemiring (x +N 0) 0) (Semiring.commutative ℕSemiring x 0))
+
+*ZZeroLeft : (a : ℤ) → nonneg 0 *Z a ≡ nonneg 0
+*ZZeroLeft (nonneg x) = refl
+*ZZeroLeft (negSucc x) = refl
+
+*ZZeroRight : (a : ℤ) → a *Z nonneg 0 ≡ nonneg 0
+*ZZeroRight (nonneg x) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring x)
+*ZZeroRight (negSucc x) = refl
+
+*ZAssociative : (a b c : ℤ) → a *Z (b *Z c) ≡ (a *Z b) *Z c
+*ZAssociative (nonneg zero) b c = transitivity (*ZZeroLeft (b *Z c)) (transitivity (equalityCommutative (*ZZeroLeft c)) (applyEquality (_*Z c) (equalityCommutative (*ZZeroLeft b))))
+*ZAssociative (nonneg (succ a)) (nonneg zero) c rewrite Semiring.productZeroRight ℕSemiring a | *ZZeroLeft c | Semiring.productZeroRight ℕSemiring a = refl
+*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring b | Semiring.productZeroRight ℕSemiring (b +N a *N succ b) | Semiring.productZeroRight ℕSemiring a = refl
+*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (nonneg (succ c)) = applyEquality nonneg (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
+*ZAssociative (nonneg (succ a)) (nonneg (succ b)) (negSucc x) rewrite productDistributes' b (a *N succ b) x | Semiring.+Associative ℕSemiring x (b *N x) ((a *N succ b) *N x) | equalityCommutative (Semiring.+Associative ℕSemiring ((x +N b *N x) +N b) (a *N ((x +N b *N x) +N b)) a) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) ((a *N succ b) *N x) (b +N a *N succ b)) | equalityCommutative (Semiring.+Associative ℕSemiring (x +N b *N x) b (a *N ((x +N b *N x) +N b) +N a)) = applyEquality (λ i → negSucc ((x +N b *N x) +N i)) ans
+  where
+    ans3 : (succ b +N (succ b *N x)) *N a ≡ succ x *N (a *N succ b)
+    ans3 rewrite multiplicationNIsCommutative (succ b) x = transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a))
+    ans2 : a *N ((x +N b *N x) +N b) +N a ≡ (a *N succ b) +N (a *N succ b) *N x
+    ans2 rewrite multiplicationNIsCommutative (a *N succ b) x | Semiring.commutative ℕSemiring (succ b *N x) b | multiplicationNIsCommutative a (b +N (succ b *N x)) | Semiring.commutative ℕSemiring ((b +N (succ b *N x)) *N a) a = ans3
+    ans : b +N (a *N ((x +N b *N x) +N b) +N a) ≡ (a *N succ b) *N x +N (b +N a *N succ b)
+    ans rewrite Semiring.commutative ℕSemiring ((a *N succ b) *N x) (b +N a *N succ b) | equalityCommutative (Semiring.+Associative ℕSemiring b (a *N succ b) ((a *N succ b) *N x)) = applyEquality (b +N_) ans2
+*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg zero) = applyEquality nonneg (Semiring.productZeroRight ℕSemiring a)
+*ZAssociative (nonneg (succ a)) (negSucc b) (nonneg (succ c)) = applyEquality negSucc ans
+  where
+    ans4 : (b +N b *N c) +N (a *N b +N (a *N b) *N c) ≡ (b +N a *N b) +N (b *N c +N (a *N b) *N c)
+    ans4 rewrite Semiring.+Associative ℕSemiring (b +N b *N c) (a *N b) ((a *N b) *N c) | Semiring.+Associative ℕSemiring (b +N a *N b) (b *N c) ((a *N b) *N c) = applyEquality (_+N (a *N b) *N c) (transitivity (transitivity (applyEquality (_+N a *N b) (Semiring.commutative ℕSemiring b (b *N c))) (equalityCommutative (Semiring.+Associative ℕSemiring (b *N c) b (a *N b)))) (Semiring.commutative ℕSemiring (b *N c) (b +N a *N b)))
+    ans3 : ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) +N ((c +N a *N c) +N a) ≡ ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) +N ((a +N a *N c) +N c)
+    ans3 rewrite Semiring.commutative ℕSemiring (c +N a *N c) a | Semiring.commutative ℕSemiring c (a *N c) | Semiring.+Associative ℕSemiring a (a *N c) c = applyEquality (λ i → i +N ((a +N a *N c) +N c)) {(b +N b *N c) +N (a *N b +N (a *N b) *N c)} {(b +N a *N b) +N (b *N c +N (a *N b) *N c)} ans4
+    ans2 : (((b +N c *N b) +N (a *N b +N a *N (c *N b))) +N (c +N a *N c)) +N a ≡ (((b +N a *N b) +N (c *N b +N c *N (a *N b))) +N (a +N c *N a)) +N c
+    ans2 rewrite multiplicationNIsCommutative c b | multiplicationNIsCommutative c (a *N b) | Semiring.*Associative ℕSemiring a b c | multiplicationNIsCommutative c a = transitivity (equalityCommutative (Semiring.+Associative ℕSemiring ((b +N b *N c) +N (a *N b +N (a *N b) *N c)) (c +N a *N c) a)) (transitivity ans3 (Semiring.+Associative ℕSemiring ((b +N a *N b) +N (b *N c +N (a *N b) *N c)) (a +N a *N c) c))
+    ans : succ a *N ((succ c *N b) +N c) +N a ≡ succ c *N ((succ a *N b) +N a) +N c
+    ans = transitivity (applyEquality (_+N a) (productDistributes (succ a) (succ c *N b) c)) (transitivity (transitivity (applyEquality (λ i → ((((b +N c *N b) +N i) +N (c +N a *N c)) +N a)) (productDistributes a b (c *N b))) (transitivity ans2 (applyEquality (λ i → (((b +N a *N b) +N i) +N (a +N c *N a)) +N c) (equalityCommutative (productDistributes c b (a *N b)))))) (applyEquality (_+N c) (equalityCommutative (productDistributes (succ c) (succ a *N b) a))))
+*ZAssociative (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality nonneg ans
+  where
+    ans : succ a *N (succ b *N succ x) ≡ succ ((succ a *N b) +N a) *N succ x
+    ans rewrite Semiring.commutative ℕSemiring (succ a *N b) a | multiplicationNIsCommutative (succ a) b = transitivity (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)) (applyEquality (_*N succ x) {succ a *N succ b} {succ b *N succ a} (multiplicationNIsCommutative (succ a) (succ b)))
+*ZAssociative (negSucc a) (nonneg zero) c rewrite *ZZeroLeft c = refl
+*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite multiplicationNIsCommutative b 0 = refl
+*ZAssociative (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc ans
+  where
+    ans2 : (d : ℕ) → ((succ b *N d) *N a) +N b *N d ≡ d *N ((succ b *N a) +N b)
+    ans2 d = transitivity (transitivity (applyEquality (((d +N b *N d) *N a) +N_) (multiplicationNIsCommutative b d)) (applyEquality (_+N d *N b) (transitivity (applyEquality (_*N a) {d +N b *N d} {d *N succ b} (multiplicationNIsCommutative (succ b) d)) (equalityCommutative (Semiring.*Associative ℕSemiring d (succ b) a))))) (equalityCommutative (Semiring.+DistributesOver* ℕSemiring d (succ b *N a) b))
+    ans : (succ (c +N b *N succ c) *N a) +N (c +N b *N succ c) ≡ (succ c *N ((succ b *N a) +N b)) +N c
+    ans rewrite Semiring.commutative ℕSemiring c (b *N succ c) | Semiring.+Associative ℕSemiring (succ (b *N succ c +N c) *N a) (b *N succ c) c | Semiring.commutative ℕSemiring (b *N succ c) c = applyEquality (_+N c) (ans2 (succ c))
+*ZAssociative (negSucc a) (nonneg (succ b)) (negSucc c) = applyEquality nonneg ans
+  where
+    ans : succ a *N ((succ ((succ b) *N c)) +N b) ≡ (succ (succ b *N a) +N b) *N succ c
+    ans rewrite Semiring.commutative ℕSemiring (succ b *N a) b | multiplicationNIsCommutative (succ b) a = transitivity (applyEquality (succ a *N_) (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring c (b *N c) b)) (applyEquality (c +N_) (transitivity (transitivity (Semiring.commutative ℕSemiring (b *N c) b) (applyEquality (b +N_) (multiplicationNIsCommutative b c))) (multiplicationNIsCommutative (succ c) b)))))) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ c))
+*ZAssociative (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring (b +N a *N succ b) = refl
+*ZAssociative (negSucc a) (negSucc b) (nonneg (succ x)) = applyEquality nonneg (transitivity (applyEquality (succ a *N_) ans) (Semiring.*Associative ℕSemiring (succ a) (succ b) (succ x)))
+  where
+    ans : succ ((succ x *N b) +N x) ≡ (succ b *N succ x)
+    ans rewrite Semiring.commutative ℕSemiring (succ x *N b) x | multiplicationNIsCommutative (succ x) b = refl
+*ZAssociative (negSucc a) (negSucc b) (negSucc x) = applyEquality negSucc t
+  where
+    l1 : (a b c d e f g : ℕ) → (a +N b) +N d ≡ e +N (f +N g) → (a +N b) +N (c +N d) ≡ (c +N e) +N (f +N g)
+    l1 a b c d e f g pr rewrite Semiring.commutative ℕSemiring c d | Semiring.+Associative ℕSemiring (a +N b) d c | pr | Semiring.commutative ℕSemiring (e +N (f +N g)) c | Semiring.+Associative ℕSemiring c e (f +N g) = refl
+    v : (((succ b) *N succ x) *N a) ≡ (succ x) *N (a *N succ b)
+    v = transitivity (applyEquality (_*N a) (multiplicationNIsCommutative (succ b) (succ x))) (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (succ x) (succ b) a)) (applyEquality (succ x *N_) (multiplicationNIsCommutative (succ b) a)))
+    u : (a +N (x +N b *N succ x) *N a) +N b *N succ x ≡ (b +N a *N succ b) *N x +N (b +N a *N succ b)
+    u = transitivity (transitivity (transitivity (Semiring.commutative ℕSemiring (a +N (x +N b *N succ x) *N a) (b *N succ x)) (transitivity (applyEquality (_+N (a +N (x +N b *N succ x) *N a)) (multiplicationNIsCommutative b (succ x))) (transitivity (applyEquality ((b +N x *N b) +N_) v) (equalityCommutative (productDistributes (succ x) b (a *N succ b)))))) (applyEquality ((b +N a *N succ b) +N_) (multiplicationNIsCommutative x (b +N a *N succ b)))) (Semiring.commutative ℕSemiring (b +N a *N succ b) ((b +N a *N succ b) *N x))
+    t : (a +N (x +N b *N succ x) *N a) +N (x +N b *N succ x) ≡ (x +N (b +N a *N succ b) *N x) +N (b +N a *N succ b)
+    t = l1 a ((x +N b *N succ x) *N a) x (b *N succ x) ((b +N (a *N succ b)) *N x) b (a *N succ b) u
+
+multLemma : (a b : ℕ) → a *N succ b ≡ a *N b +N a
+multLemma a b rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative a b = refl
+
+negSucc+Nonneg : (a b : ℕ) → negSucc a ≡ negSucc (a +N b) +Z nonneg b
+negSucc+Nonneg zero zero = refl
+negSucc+Nonneg zero (succ b) = negSucc+Nonneg zero b
+negSucc+Nonneg (succ a) zero rewrite Semiring.commutative ℕSemiring a 0 = refl
+negSucc+Nonneg (succ a) (succ b) rewrite Semiring.commutative ℕSemiring a (succ b) | Semiring.commutative ℕSemiring b a = negSucc+Nonneg (succ a) b
+
+distLemma : (a b : ℕ) →  negSucc a *Z nonneg b ≡ negSucc ((a +N b *N a) +N b) +Z nonneg (succ a)
+distLemma a b rewrite Semiring.commutative ℕSemiring (a +N b *N a) b | Semiring.commutative ℕSemiring a (b *N a) | Semiring.+Associative ℕSemiring b (b *N a) a = transitivity u (transitivity (equalityCommutative (+ZAssociative (negSucc ((b +N b *N a) +N a)) (nonneg a) (nonneg 1))) (applyEquality ((negSucc ((b +N b *N a) +N a)) +Z_) {nonneg a +Z nonneg 1} {nonneg (succ a)} (+ZCommutative (nonneg a) (nonneg 1))))
+  where
+    v : (a b : ℕ) → negSucc a *Z nonneg b ≡ (negSucc (b +N b *N a)) +Z nonneg 1
+    v zero zero = refl
+    v zero (succ b) rewrite Semiring.productZeroRight ℕSemiring b = applyEquality negSucc (equalityCommutative (Semiring.sumZeroRight ℕSemiring b))
+    v (succ a) zero = refl
+    v (succ a) (succ b) = applyEquality negSucc (Semiring.commutative ℕSemiring (succ (a +N b *N succ a)) b)
+    u : negSucc a *Z nonneg b ≡ (negSucc ((b +N b *N a) +N a) +Z nonneg a) +Z nonneg 1
+    u = transitivity (v a b) (applyEquality (_+Z nonneg 1) (negSucc+Nonneg (b +N b *N a) a))
+
+*ZDistributesOver+Z : (a b c : ℤ) → a *Z (b +Z c) ≡ (a *Z b) +Z (a *Z c)
+*ZDistributesOver+Z (nonneg zero) b c rewrite *ZZeroLeft (b +Z c) | *ZZeroLeft b | *ZZeroLeft c = refl
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (nonneg c) rewrite Semiring.productZeroRight ℕSemiring a = refl
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (nonneg c) = applyEquality nonneg (productDistributes (succ a) (succ b) c)
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg zero) (negSucc c) rewrite Semiring.productZeroRight ℕSemiring a = refl
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productZeroRight ℕSemiring a = t a
+  where
+    t : (a : ℕ) → nonneg (succ a *N b) ≡ nonneg (succ a *N succ b) +Z negSucc a
+    t zero = refl
+    t (succ a) = transitivity (+Zinherits b (b +N a *N b)) (transitivity (applyEquality (nonneg b +Z_) (t a)) (transitivity (+ZAssociative (nonneg b) (nonneg (succ (b +N a *N succ b))) (negSucc a)) (applyEquality (_+Z negSucc a) {nonneg b +Z nonneg (succ (b +N a *N succ b))} {nonneg (b +N succ (b +N a *N succ b))} (equalityCommutative (+Zinherits b _)))))
+*ZDistributesOver+Z (nonneg (succ a)) (nonneg (succ x)) (negSucc (succ b)) = transitivity (applyEquality ((nonneg (succ a)) *Z_) (+ZCommutative (nonneg x) (negSucc b))) (transitivity (transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t) (+ZCommutative (negSucc ((b +N a *N succ b) +N a)) (nonneg (x +N a *N succ x))))
+  where
+    t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
+    t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
+*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg zero) rewrite Semiring.productZeroRight ℕSemiring a = refl
+*ZDistributesOver+Z (nonneg (succ a)) (negSucc zero) (nonneg (succ x)) rewrite Semiring.productZeroRight ℕSemiring a = t a x
+  where
+    t : (a x : ℕ) → nonneg (succ a *N x) ≡ negSucc a +Z nonneg (succ a *N succ x)
+    t zero x = refl
+    t (succ a) x with t a x
+    ... | bl rewrite +Zinherits x (a *N x) | +Zinherits x (x +N a *N x) = transitivity (transitivity (applyEquality (nonneg x +Z_) (+Zinherits x (a *N x))) (+ZCommutative (nonneg x) (nonneg x +Z nonneg (a *N x)))) (transitivity (applyEquality (_+Z nonneg x) bl) (transitivity (equalityCommutative (+ZAssociative (negSucc a) (nonneg (succ x +N a *N succ x)) (nonneg x))) (applyEquality (λ i → negSucc a +Z nonneg i) {succ (x +N a *N succ x) +N x} {x +N succ (x +N a *N succ x)} (Semiring.commutative ℕSemiring (succ (x +N a *N succ x)) x))))
+*ZDistributesOver+Z (nonneg (succ a)) (negSucc (succ b)) (nonneg (succ x)) = transitivity (*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (nonneg x)) t
+  where
+    t : negSucc ((b +N a *N b) +N a) +Z nonneg (x +N a *N x) ≡ negSucc ((b +N a *N succ b) +N a) +Z nonneg (x +N a *N succ x)
+    t rewrite multLemma a x | multLemma a b | Semiring.+Associative ℕSemiring x (a *N x) a | Semiring.+Associative ℕSemiring b (a *N b) a | Semiring.commutative ℕSemiring (x +N a *N x) a | +Zinherits a (x +N a *N x) | +ZAssociative (negSucc (((b +N a *N b) +N a) +N a)) (nonneg a) (nonneg (x +N a *N x)) = applyEquality (_+Z nonneg (x +N a *N x)) {negSucc ((b +N a *N b) +N a)} {negSucc (((b +N a *N b) +N a) +N a) +Z nonneg a} (negSucc+Nonneg ((b +N a *N b) +N a) a)
+*ZDistributesOver+Z (nonneg (succ a)) (negSucc b) (negSucc x) = applyEquality negSucc (transitivity (applyEquality (_+N a) (transitivity (productDistributes (succ a) (succ b) x) (applyEquality (_+N (x +N a *N x)) {succ b +N a *N succ b} {succ (b +N a *N b) +N a} (applyEquality succ u)))) (equalityCommutative (Semiring.+Associative ℕSemiring (succ ((b +N a *N b) +N a)) (succ a *N x) a)))
+  where
+    u : b +N a *N succ b ≡ (succ a *N b) +N a
+    u rewrite multiplicationNIsCommutative a (succ b) | Semiring.commutative ℕSemiring a (b *N a) | multiplicationNIsCommutative b a = Semiring.+Associative ℕSemiring b (a *N b) a
+*ZDistributesOver+Z (negSucc a) (nonneg zero) (nonneg x) = refl
+*ZDistributesOver+Z (negSucc a) (nonneg zero) (negSucc x) = refl
+*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg zero) rewrite Semiring.commutative ℕSemiring b 0 = refl
+*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (nonneg (succ c)) = applyEquality negSucc t
+  where
+    v : a *N b +N a *N succ c ≡ c *N a +N (a +N b *N a)
+    v rewrite multiplicationNIsCommutative b a | Semiring.+Associative ℕSemiring (c *N a) a (a *N b) | Semiring.commutative ℕSemiring (c *N a +N a) (a *N b) | Semiring.commutative ℕSemiring (c *N a) a = applyEquality (λ i → a *N b +N i) (transitivity (multLemma a c) (transitivity (Semiring.commutative ℕSemiring (a *N c) a) (applyEquality (a +N_) (multiplicationNIsCommutative a c))))
+    u : (a +N (b +N succ c) *N a) +N b ≡ (a +N c *N a) +N ((a +N b *N a) +N b)
+    u rewrite Semiring.+Associative ℕSemiring (a +N c *N a) (a +N b *N a) b | (equalityCommutative (Semiring.+Associative ℕSemiring a (c *N a) (a +N b *N a))) = applyEquality (λ i → (a +N i) +N b) (transitivity (multiplicationNIsCommutative (b +N succ c) a) (transitivity (productDistributes a b (succ c)) v))
+    t : (a +N (b +N succ c) *N a) +N (b +N succ c) ≡ succ (((a +N b *N a) +N b) +N ((a +N c *N a) +N c))
+    t rewrite Semiring.+Associative ℕSemiring ((a +N (b +N succ c) *N a)) b (succ c) | Semiring.commutative ℕSemiring ((a +N b *N a) +N b) ((a +N c *N a) +N c) | Semiring.commutative ℕSemiring (a +N c *N a) c | equalityCommutative (Semiring.+Associative ℕSemiring (succ c) (a +N c *N a) ((a +N b *N a) +N b)) | Semiring.commutative ℕSemiring (succ c) ((a +N c *N a) +N ((a +N b *N a) +N b)) = applyEquality (_+N succ c) u
+*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc zero) rewrite Semiring.productOneRight ℕSemiring a = distLemma a b
+*ZDistributesOver+Z (negSucc a) (nonneg (succ b)) (negSucc (succ c)) = transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))
+  where
+    t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
+    t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
+*ZDistributesOver+Z (negSucc a) (negSucc b) (nonneg zero) rewrite Semiring.commutative ℕSemiring (b +N a *N succ b) 0 = refl
+*ZDistributesOver+Z (negSucc a) (negSucc zero) (nonneg (succ b)) = transitivity (distLemma a b) (transitivity (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a))) (applyEquality (λ i → nonneg (succ i) +Z negSucc ((a +N b *N a) +N b)) (equalityCommutative (Semiring.productOneRight ℕSemiring a))))
+*ZDistributesOver+Z (negSucc a) (negSucc (succ c)) (nonneg (succ b)) = transitivity (applyEquality (negSucc a *Z_) (+ZCommutative (negSucc c) (nonneg b))) (transitivity (transitivity (*ZDistributesOver+Z (negSucc a) (nonneg b) (negSucc c)) (transitivity (applyEquality (_+Z nonneg (succ (c +N a *N succ c))) (distLemma a b)) (transitivity (equalityCommutative (+ZAssociative (negSucc ((a +N b *N a) +N b)) (nonneg (succ a)) (nonneg (succ (c +N a *N succ c))))) (applyEquality (negSucc ((a +N b *N a) +N b) +Z_) {nonneg (succ (a +N succ (c +N a *N succ c)))} {nonneg (succ (succ (c +N a *N succ (succ c))))} (applyEquality nonneg (t (succ a) (succ c))))))) (+ZCommutative (negSucc ((a +N b *N a) +N b)) (nonneg (succ (succ (c +N a *N succ (succ c)))))))
+  where
+    t : (x y : ℕ) → x +N x *N y ≡ x *N succ y
+    t x y = transitivity (Semiring.commutative ℕSemiring x (x *N y)) (equalityCommutative (multLemma x y))
+*ZDistributesOver+Z (negSucc a) (negSucc b) (negSucc c) = applyEquality nonneg (transitivity (applyEquality (λ i → succ a *N (succ i)) (transitivity (applyEquality succ (Semiring.commutative ℕSemiring b c)) (Semiring.commutative ℕSemiring (succ c) b))) (productDistributes (succ a) (succ b) (succ c)))
+
+ℤRing : Ring (reflSetoid ℤ) _+Z_ _*Z_
+Ring.additiveGroup ℤRing = ℤGroup
+Ring.*WellDefined ℤRing refl refl = refl
+Ring.1R ℤRing = nonneg 1
+Ring.groupIsAbelian ℤRing {a} {b} = +ZCommutative a b
+Ring.*Associative ℤRing {a} {b} {c} = *ZAssociative a b c
+Ring.*Commutative ℤRing {a} {b} = *ZCommutative a b
+Ring.*DistributesOver+ ℤRing {a} {b} {c} = *ZDistributesOver+Z a b c
+Ring.identIsIdent ℤRing {a} = *ZleftIdent a
diff --git a/Numbers/Naturals/Definition.agda b/Numbers/Naturals/Definition.agda
index ea57fb6..f56f317 100644
--- a/Numbers/Naturals/Definition.agda
+++ b/Numbers/Naturals/Definition.agda
@@ -21,3 +21,11 @@ naughtE ()
 aIsNotSuccA : (a : ℕ) → (a ≡ succ a) → False
 aIsNotSuccA zero pr = naughtE pr
 aIsNotSuccA (succ a) pr = aIsNotSuccA a (succInjective pr)
+
+ℕDecideEquality : (a b : ℕ) → ((a ≡ b) || ((a ≡ b) → False))
+ℕDecideEquality zero zero = inl refl
+ℕDecideEquality zero (succ b) = inr (λ ())
+ℕDecideEquality (succ a) zero = inr (λ ())
+ℕDecideEquality (succ a) (succ b) with ℕDecideEquality a b
+ℕDecideEquality (succ a) (succ b) | inl x = inl (applyEquality succ x)
+ℕDecideEquality (succ a) (succ b) | inr x = inr λ pr → x (succInjective pr)
diff --git a/Numbers/Rationals/Lemmas.agda b/Numbers/Rationals/Lemmas.agda
index 36242bd..29eb7b3 100644
--- a/Numbers/Rationals/Lemmas.agda
+++ b/Numbers/Rationals/Lemmas.agda
@@ -6,6 +6,7 @@ open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
 open import Numbers.Naturals.Order.WellFounded
 open import Numbers.Naturals.Order.Lemmas
+open import Numbers.Integers.Definition
 open import Numbers.Integers.Integers
 open import Numbers.Integers.Order
 open import Groups.Groups
diff --git a/Rings/Definition.agda b/Rings/Definition.agda
index 1fcd357..de39635 100644
--- a/Rings/Definition.agda
+++ b/Rings/Definition.agda
@@ -14,49 +14,26 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 
 -- Following Part IB's course Groups, Rings, and Modules, we take rings to be commutative with one.
 module Rings.Definition where
-  record Ring {n m} {A : Set n} (S : Setoid {n} {m} A) (_+_ : A → A → A) (_*_ : A → A → A) : Set (lsuc n ⊔ m) where
-    field
-      additiveGroup : Group S _+_
-    open Group additiveGroup
-    open Setoid S
-    open Equivalence eq
-    0R : A
-    0R = 0G
-    _-R_ : A → A → A
-    a -R b = a + (inverse b)
-    field
-      *WellDefined : {r s t u : A} → (r ∼ t) → (s ∼ u) → r * s ∼ t * u
-      1R : A
-      groupIsAbelian : {a b : A} → a + b ∼ b + a
-      *Associative : {a b c : A} → (a * (b * c)) ∼ (a * b) * c
-      *Commutative : {a b : A} → a * b ∼ b * a
-      *DistributesOver+ : {a b c : A} → a * (b + c) ∼ (a * b) + (a * c)
-      identIsIdent : {a : A} → 1R * a ∼ a
-    timesZero : {a : A} → a * 0R ∼ 0R
-    timesZero {a} = symmetric (transitive (transitive (symmetric invLeft) (+WellDefined reflexive (transitive (*WellDefined {a} {a} reflexive (symmetric identRight)) *DistributesOver+))) (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft)))
 
-
-  --directSumRing : {m n : _} → {A : Set m} {B : Set n} (r : Ring A) (s : Ring B) → Ring (A && B)
-  --Ring.additiveGroup (directSumRing r s) = directSumGroup (Ring.additiveGroup r) (Ring.additiveGroup s)
-  --Ring._*_ (directSumRing r s) (a ,, b) (c ,, d) = (Ring._*_ r a c) ,, Ring._*_ s b d
-  --Ring.multWellDefined (directSumRing r s) (a ,, b) (c ,, d) = Ring.multWellDefined r a c ,, Ring.multWellDefined s b d
-  --Ring.1R (directSumRing r s) = Ring.1R r ,, Ring.1R s
-  --Ring.groupIsAbelian (directSumRing r s) = Ring.groupIsAbelian r ,, Ring.groupIsAbelian s
-  --Ring.assoc (directSumRing r s) = Ring.assoc r ,, Ring.assoc s
-  --Ring.multCommutative (directSumRing r s) = Ring.multCommutative r ,, Ring.multCommutative s
-  --Ring.multDistributes (directSumRing r s) = Ring.multDistributes r ,, Ring.multDistributes s
-  --Ring.identIsIdent (directSumRing r s) = Ring.identIsIdent r ,, Ring.identIsIdent s
-
-  record RingHom {m n o p : _} {A : Set m} {B : Set n} {SA : Setoid {m} {o} A} {SB : Setoid {n} {p} B} {_+A_ : A → A → A} {_*A_ : A → A → A} (R : Ring SA _+A_ _*A_) {_+B_ : B → B → B} {_*B_ : B → B → B} (S : Ring SB _+B_ _*B_) (f : A → B) : Set (m ⊔ n ⊔ o ⊔ p) where
-    open Ring S
-    open Group additiveGroup
-    open Setoid SB
-    field
-      preserves1 : f (Ring.1R R) ∼ 1R
-      ringHom : {r s : A} → f (r *A s) ∼ (f r) *B (f s)
-      groupHom : GroupHom (Ring.additiveGroup R) additiveGroup f
-
-  --record RingIso {m n : _} {A : Set m} {B : Set n} (R : Ring A) (S : Ring B) (f : A → B) : Set (m ⊔ n) where
-  --  field
-  --    ringHom : RingHom R S f
-  --    bijective : Bijection f
+record Ring {n m} {A : Set n} (S : Setoid {n} {m} A) (_+_ : A → A → A) (_*_ : A → A → A) : Set (lsuc n ⊔ m) where
+  field
+    additiveGroup : Group S _+_
+  open Group additiveGroup
+  open Setoid S
+  open Equivalence eq
+  0R : A
+  0R = 0G
+  _-R_ : A → A → A
+  a -R b = a + (inverse b)
+  field
+    *WellDefined : {r s t u : A} → (r ∼ t) → (s ∼ u) → r * s ∼ t * u
+    1R : A
+    groupIsAbelian : {a b : A} → a + b ∼ b + a
+    *Associative : {a b c : A} → (a * (b * c)) ∼ (a * b) * c
+    *Commutative : {a b : A} → a * b ∼ b * a
+    *DistributesOver+ : {a b c : A} → a * (b + c) ∼ (a * b) + (a * c)
+    identIsIdent : {a : A} → 1R * a ∼ a
+  timesZero : {a : A} → a * 0R ∼ 0R
+  timesZero {a} = symmetric (transitive (transitive (symmetric invLeft) (+WellDefined reflexive (transitive (*WellDefined {a} {a} reflexive (symmetric identRight)) *DistributesOver+))) (transitive +Associative (transitive (+WellDefined invLeft reflexive) identLeft)))
+  *DistributesOver+' : {a b c : A} → (a + b) * c ∼ (a * c) + (b * c)
+  *DistributesOver+' = transitive *Commutative (transitive *DistributesOver+ (+WellDefined *Commutative *Commutative))
diff --git a/Rings/Homomorphisms/Definition.agda b/Rings/Homomorphisms/Definition.agda
new file mode 100644
index 0000000..4d991e8
--- /dev/null
+++ b/Rings/Homomorphisms/Definition.agda
@@ -0,0 +1,26 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Naturals
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+-- Following Part IB's course Groups, Rings, and Modules, we take rings to be commutative with one.
+module Rings.Homomorphisms.Definition where
+
+record RingHom {m n o p : _} {A : Set m} {B : Set n} {SA : Setoid {m} {o} A} {SB : Setoid {n} {p} B} {_+A_ : A → A → A} {_*A_ : A → A → A} (R : Ring SA _+A_ _*A_) {_+B_ : B → B → B} {_*B_ : B → B → B} (S : Ring SB _+B_ _*B_) (f : A → B) : Set (m ⊔ n ⊔ o ⊔ p) where
+  open Ring S
+  open Group additiveGroup
+  open Setoid SB
+  field
+    preserves1 : f (Ring.1R R) ∼ 1R
+    ringHom : {r s : A} → f (r *A s) ∼ (f r) *B (f s)
+    groupHom : GroupHom (Ring.additiveGroup R) additiveGroup f
diff --git a/Rings/Ideals/Definition.agda b/Rings/Ideals/Definition.agda
new file mode 100644
index 0000000..fc30077
--- /dev/null
+++ b/Rings/Ideals/Definition.agda
@@ -0,0 +1,20 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Naturals
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Rings.Homomorphisms.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Ideals.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+ringKernel : {c d : _} {C : Set c} {T : Setoid {c} {d} C} {_+2_ _*2_ : C → C → C} (R2 : Ring T _+2_ _*2_) {f : A → C} (fHom : RingHom R R2 f) → Set (a ⊔ d)
+ringKernel {T = T} R2 {f} fHom = Sg A (λ a → Setoid._∼_ T (f a) (Ring.0R R2))
diff --git a/Rings/Isomorphisms/Definition.agda b/Rings/Isomorphisms/Definition.agda
new file mode 100644
index 0000000..af5f08d
--- /dev/null
+++ b/Rings/Isomorphisms/Definition.agda
@@ -0,0 +1,22 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Naturals
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Rings.Homomorphisms.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Isomorphisms.Definition {a b c d : _} {A : Set a} {S : Setoid {a} {b} A} {_+1_ _*1_ : A → A → A} (R1 : Ring S _+1_ _*1_) {B : Set c} {T : Setoid {c} {d} B} {_+2_ _*2_ : B → B → B} (R2 : Ring T _+2_ _*2_) where
+
+record RingIso (f : A → B) : Set (a ⊔ b ⊔ c ⊔ d) where
+  field
+    ringHom : RingHom R1 R2 f
+    bijective : Bijection f
diff --git a/Rings/Polynomial/Definition.agda b/Rings/Polynomial/Definition.agda
new file mode 100644
index 0000000..cd4ed72
--- /dev/null
+++ b/Rings/Polynomial/Definition.agda
@@ -0,0 +1,33 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Definition
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Vectors
+open import Lists.Lists
+open import Maybe
+open import Rings.Homomorphisms.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Polynomial.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+open Setoid S
+open Equivalence eq
+open Ring R
+
+open import Groups.Polynomials.Definition additiveGroup
+
+1P : NaivePoly
+1P = 1R :: []
+
+inducedFunction : NaivePoly → A → A
+inducedFunction [] a = 0R
+inducedFunction (x :: p) a = x + (a * inducedFunction p a)
diff --git a/Rings/Polynomial/Multiplication.agda b/Rings/Polynomial/Multiplication.agda
new file mode 100644
index 0000000..9a89931
--- /dev/null
+++ b/Rings/Polynomial/Multiplication.agda
@@ -0,0 +1,123 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Abelian.Definition
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Definition
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Vectors
+open import Lists.Lists
+open import Maybe
+open import Rings.Homomorphisms.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Polynomial.Multiplication {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+open Ring R
+open Group additiveGroup
+open import Groups.Polynomials.Definition additiveGroup
+open import Groups.Polynomials.Group additiveGroup
+open Setoid S
+open Equivalence eq
+
+_*P_ : NaivePoly → NaivePoly → NaivePoly
+[] *P b = []
+(x :: a) *P [] = []
+(x :: a) *P (y :: b) = (x * y) :: ((map (x *_) b) +P (map (y *_) a))
+
+p*Commutative : {a b : NaivePoly} → polysEqual (a *P b) (b *P a)
+p*Commutative {[]} {[]} = record {}
+p*Commutative {[]} {x :: b} = record {}
+p*Commutative {x :: a} {[]} = record {}
+p*Commutative {x :: xs} {y :: ys} = *Commutative ,, AbelianGroup.commutative (abelian (record { commutative = Ring.groupIsAbelian R })) {map (_*_ x) ys} {map (_*_ y) xs}
+
+zeroTimes1 : {a : NaivePoly} (c : A) → (c ∼ 0G) → polysEqual (map (_*_ c) a) []
+zeroTimes1 {[]} c c=0 = record {}
+zeroTimes1 {x :: a} c c=0 = transitive (transitive *Commutative (*WellDefined reflexive c=0)) (timesZero {x}) ,, zeroTimes1 {a} c c=0
+
+zeroTimes2 : {a : NaivePoly} (c : A) → polysEqual a [] → polysEqual (map (_*_ c) a) []
+zeroTimes2 {[]} c a=0 = record {}
+zeroTimes2 {x :: a} c (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {c}) ,, zeroTimes2 {a} c snd
+
+mapWellDefined : (a c : A) (bs : NaivePoly) → (a ∼ c) → polysEqual (map (_*_ a) bs) (map (_*_ c) bs)
+mapWellDefined a c [] a=c = record {}
+mapWellDefined a c (x :: bs) a=c = *WellDefined a=c reflexive ,, mapWellDefined a c bs a=c
+
+mapWellDefined' : (a : A) (bs cs : NaivePoly) → polysEqual bs cs → polysEqual (map (_*_ a) bs) (map (_*_ a) cs)
+mapWellDefined' a [] [] bs=cs = record {}
+mapWellDefined' a [] (x :: cs) (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {a}) ,, Equivalence.symmetric (Setoid.eq naivePolySetoid) (zeroTimes2 {cs} a (Equivalence.symmetric (Setoid.eq naivePolySetoid) snd))
+mapWellDefined' a (x :: bs) [] (fst ,, snd) = transitive (*WellDefined reflexive fst) (timesZero {a}) ,, zeroTimes2 {bs} a snd
+mapWellDefined' a (b :: bs) (c :: cs) (fst ,, snd) = *WellDefined reflexive fst ,, mapWellDefined' a bs cs snd
+
+*PwellDefinedL : {a b c : NaivePoly} → polysEqual a c → polysEqual (a *P b) (c *P b)
+*PwellDefinedL {[]} {[]} {[]} a=c = record {}
+*PwellDefinedL {[]} {[]} {x :: c} a=c = record {}
+*PwellDefinedL {[]} {x :: b} {[]} a=c = record {}
+*PwellDefinedL {[]} {b :: bs} {c :: cs} (fst ,, snd) = transitive (transitive *Commutative (*WellDefined reflexive fst)) (timesZero {b}) ,, Equivalence.symmetric (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined (zeroTimes1 {bs} c fst) (zeroTimes2 {cs} b (Equivalence.symmetric (Setoid.eq naivePolySetoid) snd))) (Group.identLeft polyGroup))
+*PwellDefinedL {a :: as} {[]} {[]} a=c = record {}
+*PwellDefinedL {a :: as} {[]} {x :: c} a=c = record {}
+*PwellDefinedL {a :: as} {b :: bs} {[]} (fst ,, snd) = transitive (transitive *Commutative (*WellDefined reflexive fst)) (timesZero {b}) ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined (zeroTimes1 {bs} a fst) (zeroTimes2 {as} b snd)) (Group.identLeft polyGroup)
+*PwellDefinedL {a :: as} {b :: bs} {c :: cs} (fst ,, snd) = *WellDefined fst reflexive ,, +PwellDefined (mapWellDefined a c bs fst) (mapWellDefined' b as cs snd)
+
+*PwellDefinedR : {a b c : NaivePoly} → polysEqual b c → polysEqual (a *P b) (a *P c)
+*PwellDefinedR {a} {b} {c} b=c = Equivalence.transitive (Setoid.eq naivePolySetoid) (p*Commutative {a} {b}) (Equivalence.transitive (Setoid.eq naivePolySetoid) (*PwellDefinedL b=c) (p*Commutative {c} {a}))
+
+*PwellDefined : {a b c d : NaivePoly} → polysEqual a c → polysEqual b d → polysEqual (a *P b) (c *P d)
+*PwellDefined {a}{b}{c}{d} a=c b=d = Equivalence.transitive (Setoid.eq naivePolySetoid) (*PwellDefinedL a=c) (*PwellDefinedR b=d)
+
+private
+  *1 : (a : NaivePoly) → polysEqual (map (_*_ 1R) a) a
+  *1 [] = record {}
+  *1 (x :: a) = Ring.identIsIdent R ,, *1 a
+
+*Pident : {a : NaivePoly} → polysEqual ((1R :: []) *P a) a
+*Pident {[]} = record {}
+*Pident {x :: a} = Ring.identIsIdent R ,, (Equivalence.transitive (Setoid.eq naivePolySetoid) (Group.identRight polyGroup {map (_*_ 1R) a}) (*1 a))
+
+private
+  mapMap' : (f g : A → A) (xs : NaivePoly) → map f (map g xs) ≡ map (λ x → f (g x)) xs
+  mapMap' f g [] = refl
+  mapMap' f g (x :: xs) rewrite mapMap' f g xs = refl
+
+  mapDist : (f : A → A) (fDist : {x y : A} → f (x + y) ∼ (f x) + (f y)) (xs ys : NaivePoly) → polysEqual (map f (xs +P ys)) ((map f xs) +P (map f ys))
+  mapDist f fDist [] [] = record {}
+  mapDist f fDist [] (x :: ys) rewrite mapId ys | mapId (map f ys) = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
+  mapDist f fDist (x :: xs) [] rewrite mapId xs | mapId (map f xs) = reflexive ,, Equivalence.reflexive (Setoid.eq naivePolySetoid)
+  mapDist f fDist (x :: xs) (y :: ys) = fDist {x} {y} ,, mapDist f fDist xs ys
+
+  mapWd : (f g : A → A) (xs : NaivePoly) → ((x : A) → (f x) ∼ (g x)) → polysEqual (map f xs) (map g xs)
+  mapWd f g [] ext = record {}
+  mapWd f g (x :: xs) ext = ext x ,, mapWd f g xs ext
+
+  mapDist' : (b c : A) → (as : NaivePoly) → polysEqual (map (_*_ (b + c)) as) (map (_*_ c) as +P map (_*_ b) as)
+  mapDist' b c [] = record {}
+  mapDist' b c (x :: as) = transitive (Ring.*DistributesOver+' R {b} {c} {x}) groupIsAbelian ,, mapDist' b c as
+
+*Passoc : {a b c : NaivePoly} → polysEqual (a *P (b *P c)) ((a *P b) *P c)
+*Passoc {[]} {b} {c} = record {}
+*Passoc {a :: as} {[]} {c} = record {}
+*Passoc {a :: as} {b :: bs} {[]} = record {}
+*Passoc {a :: as} {b :: bs} {c :: cs} = *Associative ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined (mapDist (_*_ a) *DistributesOver+ (map (_*_ b) cs) (map (_*_ c) bs)) (Equivalence.reflexive (Setoid.eq naivePolySetoid))) (Equivalence.transitive (Setoid.eq naivePolySetoid) ans (+PwellDefined (Equivalence.reflexive (Setoid.eq naivePolySetoid) {map (_*_ (a * b)) cs}) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (mapDist (_*_ c) *DistributesOver+ (map (_*_ a) bs) (map (_*_ b) as)))))
+  where
+    ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) (map (_*_ b) cs)) (map (_*_ a) (map (_*_ c) bs))) (map (_*_ (b * c)) as)) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ (a * b)) cs) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ c) (map (_*_ a) bs)) (map (_*_ c) (map (_*_ b) as))))
+    ans rewrite mapMap' (_*_ a) (_*_ c) bs | mapMap' (_*_ a) (_*_ b) cs | mapMap' (_*_ c) (_*_ a) bs | mapMap' (_*_ c) (_*_ b) as = Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.+Associative polyGroup {map (λ x → a * (b * x)) cs} {map (λ x → a * (c * x)) bs} {map (_*_ (b * c)) as})) (+PwellDefined {map (λ x → a * (b * x)) cs} {(map (λ x → a * (c * x)) bs) +P map (_*_ (b * c)) as} {(map (_*_ (a * b)) cs)} (mapWd (λ x → a * (b * x)) (_*_ (a * b)) cs λ x → *Associative) (+PwellDefined {map (λ x → a * (c * x)) bs} {map (_*_ (b * c)) as} {map (λ x → c * (a * x)) bs} {map (λ x → c * (b * x)) as} (mapWd (λ x → a * (c * x)) (λ x → c * (a * x)) bs λ x → transitive *Commutative (transitive (symmetric *Associative) (*WellDefined reflexive *Commutative))) (mapWd (_*_ (b * c)) (λ x → c * (b * x)) as λ x → transitive (*WellDefined *Commutative reflexive) (symmetric *Associative))))
+
+*Pdistrib : {a b c : NaivePoly} → polysEqual (a *P (b +P c)) ((a *P b) +P (a *P c))
+*Pdistrib {[]} {b} {c} = record {}
+*Pdistrib {a :: as} {[]} {[]} = record {}
+*Pdistrib {a :: as} {[]} {c :: cs} = reflexive ,, ans
+  where
+    ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) (map (λ z → z) cs)) (map (_*_ c) as)) (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) cs) (map (_*_ c) as)))
+    ans rewrite mapId (listZip _+_ id id (map (_*_ a) cs) (map (_*_ c) as)) | mapId cs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
+*Pdistrib {a :: as} {b :: bs} {[]} = reflexive ,, ans
+  where
+    ans : polysEqual (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) (map (λ z → z) bs)) (map (_*_ b) as)) (map (λ z → z) (listZip _+_ (λ z → z) (λ z → z) (map (_*_ a) bs) (map (_*_ b) as)))
+    ans rewrite mapId (listZip _+_ id id (map (_*_ a) bs) (map (_*_ b) as)) | mapId bs = Equivalence.reflexive (Setoid.eq naivePolySetoid)
+*Pdistrib {a :: as} {b :: bs} {c :: cs} = *DistributesOver+ ,, Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (Equivalence.transitive (Setoid.eq naivePolySetoid) (+PwellDefined {map (_*_ a) (bs +P cs)} {map (_*_ (b + c)) as} {(map (_*_ a) bs) +P (map (_*_ a) cs)} (mapDist (_*_ a) *DistributesOver+ bs cs) (mapDist' b c as)) (Group.+Associative polyGroup {(map (_*_ a) bs) +P (map (_*_ a) cs)} {map (_*_ c) as} {map (_*_ b) as})) (+PwellDefined (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.+Associative polyGroup {map (_*_ a) bs} {map (_*_ a) cs} {map (_*_ c) as})) (Equivalence.reflexive (Setoid.eq naivePolySetoid) {map (_*_ b) as}))) (Equivalence.symmetric (Setoid.eq naivePolySetoid) (Group.+Associative polyGroup {map (_*_ a) bs} {(map (_*_ a) cs) +P (map (_*_ c) as)} {map (_*_ b) as}))) (+PwellDefined (Equivalence.reflexive (Setoid.eq naivePolySetoid) {map (_*_ a) bs}) (AbelianGroup.commutative (abelian (record { commutative = groupIsAbelian })) {map (_*_ a) cs +P map (_*_ c) as} {map (_*_ b) as}))) (Group.+Associative polyGroup {map (_*_ a) bs} {map (_*_ b) as})
diff --git a/Rings/Polynomial/Ring.agda b/Rings/Polynomial/Ring.agda
new file mode 100644
index 0000000..0810295
--- /dev/null
+++ b/Rings/Polynomial/Ring.agda
@@ -0,0 +1,45 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Abelian.Definition
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Numbers.Naturals.Definition
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Vectors
+open import Lists.Lists
+open import Maybe
+open import Rings.Homomorphisms.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Rings.Polynomial.Ring {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ _*_ : A → A → A} (R : Ring S _+_ _*_) where
+
+open Ring R
+open Setoid S
+open Equivalence eq
+open import Groups.Polynomials.Group additiveGroup
+open import Groups.Polynomials.Definition additiveGroup
+open import Rings.Polynomial.Definition R
+open import Rings.Polynomial.Multiplication R
+
+polyRing : Ring naivePolySetoid _+P_ _*P_
+Ring.additiveGroup polyRing = polyGroup
+Ring.*WellDefined polyRing {a} {b} {c} {d} = *PwellDefined {a} {b} {c} {d}
+Ring.1R polyRing = 1R :: []
+Ring.groupIsAbelian polyRing {x} {y} = AbelianGroup.commutative (abelian (record { commutative = Ring.groupIsAbelian R })) {x} {y}
+Ring.*Associative polyRing {a} {b} {c} = *Passoc {a} {b} {c}
+Ring.*Commutative polyRing {a} {b} = p*Commutative {a} {b}
+Ring.*DistributesOver+ polyRing {a} {b} {c} = *Pdistrib {a} {b} {c}
+Ring.identIsIdent polyRing {a} = *Pident {a}
+
+polyInjectionIsHom : RingHom R polyRing polyInjection
+RingHom.preserves1 polyInjectionIsHom = reflexive ,, record {}
+RingHom.ringHom polyInjectionIsHom = reflexive ,, record {}
+GroupHom.groupHom (RingHom.groupHom polyInjectionIsHom) = reflexive ,, record {}
+GroupHom.wellDefined (RingHom.groupHom polyInjectionIsHom) = SetoidInjection.wellDefined polyInjectionIsInj
diff --git a/Vectors.agda b/Vectors.agda
index c39160b..beaf28e 100644
--- a/Vectors.agda
+++ b/Vectors.agda
@@ -6,6 +6,7 @@ open import Numbers.Naturals.Order
 open import Functions
 open import Semirings.Definition
 open import Orders
+open import Lists.Lists
 
 data Vec {a : _} (X : Set a) : ℕ -> Set a where
   [] : Vec X zero
@@ -38,6 +39,9 @@ vecLast {a} {X} {zero} v ()
 vecLast {a} {X} {succ zero} (x ,- []) _ = x
 vecLast {a} {X} {succ (succ m)} (x ,- v) _ = vecLast v (succIsPositive m)
 
+vecLast' : {a : _} {X : Set a} {m : ℕ} → Vec X (succ m) → X
+vecLast' {m = m} v = vecLast v (le m (applyEquality succ (Semiring.sumZeroRight ℕSemiring m)))
+
 vecAppend : {a : _} {X : Set a} {m : ℕ} → Vec X m → (x : X) → Vec X (succ m)
 vecAppend {a} {X} {zero} [] x = x ,- []
 vecAppend {a} {X} {succ m} (y ,- v) x = y ,- vecAppend v x
@@ -54,9 +58,9 @@ vecMoveAppend : {a : _} {X : Set a} {m : ℕ} → (x : X) → (v : Vec X m) →
 vecMoveAppend {a} {X} {.0} x [] = refl
 vecMoveAppend {a} {X} {.(succ _)} x (y ,- v) rewrite vecMoveAppend x v = refl
 
-revRevIsId : {a : _} {X : Set a} {m : ℕ} → (v : Vec X m) → (vecRev (vecRev v)) ≡ v
-revRevIsId {a} {X} {zero} [] = refl
-revRevIsId {a} {X} {succ m} (x ,- v) rewrite vecMoveAppend x (vecRev v) = applyEquality (λ i → x ,- i) (revRevIsId v)
+vecRevRevIsId : {a : _} {X : Set a} {m : ℕ} → (v : Vec X m) → (vecRev (vecRev v)) ≡ v
+vecRevRevIsId {a} {X} {zero} [] = refl
+vecRevRevIsId {a} {X} {succ m} (x ,- v) rewrite vecMoveAppend x (vecRev v) = applyEquality (λ i → x ,- i) (vecRevRevIsId v)
 
 record vecContains {a : _} {X : Set a} {m : ℕ} (vec : Vec X m) (x : X) : Set a where
   field
@@ -153,6 +157,10 @@ vecComposition : {a b c : _} {X : Set a} {Y : Set b} {Z : Set c} {n : ℕ} (fs :
 vecComposition [] [] [] = refl
 vecComposition (f ,- fs) (g ,- gs) (x ,- xs) rewrite vecComposition fs gs xs = refl
 
+vecToList : {a : _} {A : Set a} {n : ℕ} → (v : Vec A n) → List A
+vecToList [] = []
+vecToList (x ,- v) = x :: vecToList v
+
 ------------
 
 data _<=_ : ℕ → ℕ → Set where