diff --git a/Groups/Cyclic/Definition.agda b/Groups/Cyclic/Definition.agda
index eb37bdc..5ac6973 100644
--- a/Groups/Cyclic/Definition.agda
+++ b/Groups/Cyclic/Definition.agda
@@ -14,6 +14,7 @@ open import Groups.Groups
 open import Groups.Subgroups.Definition
 open import Groups.Abelian.Definition
 open import Groups.Definition
+open import Groups.Lemmas
 
 module Groups.Cyclic.Definition {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) where
 
@@ -25,6 +26,10 @@ positiveEltPower : (x : A) (i : ℕ) → A
 positiveEltPower x 0 = Group.0G G
 positiveEltPower x (succ i) = x · (positiveEltPower x i)
 
+positiveEltPowerWellDefinedG : (x y : A) → (x ∼ y) → (i : ℕ) → (positiveEltPower x i) ∼ (positiveEltPower y i)
+positiveEltPowerWellDefinedG x y x=y 0 = reflexive
+positiveEltPowerWellDefinedG x y x=y (succ i) = +WellDefined x=y (positiveEltPowerWellDefinedG x y x=y i)
+
 positiveEltPowerCollapse : (x : A) (i j : ℕ) → Setoid._∼_ S ((positiveEltPower x i) · (positiveEltPower x j)) (positiveEltPower x (i +N j))
 positiveEltPowerCollapse x zero j = Group.identLeft G
 positiveEltPowerCollapse x (succ i) j = transitive (symmetric +Associative) (+WellDefined reflexive (positiveEltPowerCollapse x i j))
@@ -33,6 +38,17 @@ elementPower : (x : A) (i : ℤ) → A
 elementPower x (nonneg i) = positiveEltPower x i
 elementPower x (negSucc i) = Group.inverse G (positiveEltPower x (succ i))
 
+-- TODO: move this to lemmas
+elementPowerWellDefinedZ : (i j : ℤ) → (i ≡ j) → {g : A} → elementPower g i ≡ elementPower g j
+elementPowerWellDefinedZ i j i=j {g} = applyEquality (elementPower g) i=j
+
+elementPowerWellDefinedZ' : (i j : ℤ) → (i ≡ j) → {g : A} → (elementPower g i) ∼ (elementPower g j)
+elementPowerWellDefinedZ' i j i=j {g} = identityOfIndiscernablesRight _∼_ reflexive (elementPowerWellDefinedZ i j i=j)
+
+elementPowerWellDefinedG : (g h : A) → (g ∼ h) → {n : ℤ} → (elementPower g n) ∼ (elementPower h n)
+elementPowerWellDefinedG g h g=h {nonneg n} = positiveEltPowerWellDefinedG g h g=h n
+elementPowerWellDefinedG g h g=h {negSucc x} = inverseWellDefined G (+WellDefined g=h (positiveEltPowerWellDefinedG g h g=h x))
+
 record CyclicGroup : Set (m ⊔ n) where
   field
     generator : A
diff --git a/Groups/Cyclic/DefinitionLemmas.agda b/Groups/Cyclic/DefinitionLemmas.agda
index a042350..0b7b27d 100644
--- a/Groups/Cyclic/DefinitionLemmas.agda
+++ b/Groups/Cyclic/DefinitionLemmas.agda
@@ -39,3 +39,30 @@ elementPowerCollapse x (negSucc (succ a)) (nonneg zero) = identRight
 elementPowerCollapse x (negSucc (succ a)) (nonneg (succ b)) = transitive (transitive +Associative (+WellDefined (transitive (+WellDefined (invContravariant G) reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invLeft) identRight))) reflexive)) (elementPowerCollapse x (negSucc a) (nonneg b))
 elementPowerCollapse x (negSucc a) (negSucc b) = transitive (+WellDefined reflexive (invContravariant G)) (transitive (transitive (transitive +Associative (+WellDefined (transitive (symmetric (invContravariant G)) (transitive (inverseWellDefined G +Associative) (transitive (inverseWellDefined G (+WellDefined (symmetric (elementPowerCommutes x b)) reflexive)) (transitive (inverseWellDefined G (symmetric +Associative)) (transitive (invContravariant G) (+WellDefined (inverseWellDefined G (transitive (positiveEltPowerCollapse G x b a) (identityOfIndiscernablesRight _∼_ reflexive (applyEquality (positiveEltPower G x) {b +N a} {a +N b} (Semiring.commutative ℕSemiring b a))))) reflexive)))))) reflexive)) (+WellDefined (symmetric (invContravariant G)) reflexive)) (symmetric (invContravariant G)))
 
+positiveEltPowerInverse : (m : ℕ) → (x : A) → (positiveEltPower G (inverse x) m) ∼ inverse (positiveEltPower G x m)
+positiveEltPowerInverse zero x = symmetric (invIdent G)
+positiveEltPowerInverse (succ m) x = transitive (+WellDefined reflexive (positiveEltPowerInverse m x)) (transitive (symmetric (invContravariant G)) (inverseWellDefined G (symmetric (elementPowerCommutes x m))))
+
+positiveEltPowerMultiplies : (m n : ℕ) → (x : A) → (positiveEltPower G x (m *N n)) ∼ (positiveEltPower G (positiveEltPower G x n) m)
+positiveEltPowerMultiplies zero n x = reflexive
+positiveEltPowerMultiplies (succ m) n x = transitive (symmetric (positiveEltPowerCollapse G x n (m *N n))) (+WellDefined reflexive (positiveEltPowerMultiplies m n x))
+
+powerZero : (m : ℕ) → positiveEltPower G 0G m ∼ 0G
+powerZero zero = reflexive
+powerZero (succ m) = transitive identLeft (powerZero m)
+
+elementPowerMultiplies : (m n : ℤ) → (x : A) → (elementPower G x (m *Z n)) ∼ (elementPower G (elementPower G x n) m)
+elementPowerMultiplies (nonneg m) (nonneg n) x = positiveEltPowerMultiplies m n x
+elementPowerMultiplies (nonneg zero) (negSucc n) x = reflexive
+elementPowerMultiplies (nonneg (succ m)) (negSucc n) x =  transitive (transitive (inverseWellDefined G (transitive (transitive (elementPowerWellDefinedZ' G (nonneg (succ (n +N m *N n) +N m)) (nonneg (m *N succ n +N succ n)) (applyEquality nonneg (transitivity (applyEquality succ (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring n (m *N n) m)) (applyEquality (n +N_) (transitivity (transitivity (Semiring.commutative ℕSemiring _ m) (applyEquality (m +N_) (multiplicationNIsCommutative m n))) (multiplicationNIsCommutative (succ n) m))))) (Semiring.commutative ℕSemiring (succ n) _))) {x}) (symmetric (positiveEltPowerCollapse G x (m *N succ n) (succ n)))) (+WellDefined (positiveEltPowerMultiplies m (succ n) x) reflexive))) (invContravariant G)) (+WellDefined reflexive (symmetric (positiveEltPowerInverse m (x + positiveEltPower G x n))))
+elementPowerMultiplies (negSucc m) (nonneg zero) r = transitive (symmetric (invIdent G)) (inverseWellDefined G (transitive (symmetric identLeft) (+WellDefined reflexive (symmetric (powerZero m)))))
+elementPowerMultiplies (negSucc m) (nonneg (succ n)) x = inverseWellDefined G (transitive (transitive (+WellDefined reflexive (transitive (elementPowerWellDefinedZ' G (nonneg ((m +N n *N m) +N n)) (nonneg (n +N m *N succ n)) (applyEquality nonneg (transitivity (Semiring.commutative ℕSemiring _ n) (applyEquality (n +N_) (multiplicationNIsCommutative _ m)))) {x}) (symmetric (positiveEltPowerCollapse G x n (m *N succ n))))) +Associative) (+WellDefined reflexive (positiveEltPowerMultiplies m (succ n) x)))
+elementPowerMultiplies (negSucc m) (negSucc n) r = transitive (transitive (transitive (transitive (elementPowerWellDefinedZ' G (nonneg (succ m *N succ n)) (nonneg (m *N succ n +N succ n)) (applyEquality nonneg (Semiring.commutative ℕSemiring (succ n) _)) {r}) (symmetric (positiveEltPowerCollapse G r (m *N succ n) (succ n)))) (transitive (elementPowerCollapse r (nonneg (m *N succ n)) (nonneg (succ n))) (transitive (transitive (elementPowerWellDefinedZ' G (nonneg (m *N succ n) +Z nonneg (succ n)) (nonneg (m *N succ n +N succ n)) (equalityCommutative (+Zinherits (m *N succ n) (succ n))) {r}) (symmetric (positiveEltPowerCollapse G r (m *N succ n) (succ n)))) (+WellDefined (positiveEltPowerMultiplies m (succ n) r) reflexive)))) (+WellDefined (transitive (symmetric (invTwice G _)) (inverseWellDefined G (symmetric (positiveEltPowerInverse m (r + positiveEltPower G r n))))) (symmetric (invTwice G _)))) (symmetric (invContravariant G))
+
+positiveEltPowerHomAbelian : ({x y : A} → (x + y) ∼ (y + x)) → (x y : A) → (r : ℕ) → (positiveEltPower G (x + y) r) ∼ (positiveEltPower G x r + positiveEltPower G y r)
+positiveEltPowerHomAbelian ab x y zero = symmetric identRight
+positiveEltPowerHomAbelian ab x y (succ r) = transitive (symmetric +Associative) (transitive (+WellDefined reflexive (transitive (+WellDefined reflexive (positiveEltPowerHomAbelian ab x y r)) (transitive (+WellDefined reflexive ab) (transitive +Associative ab)))) +Associative)
+
+elementPowerHomAbelian : ({x y : A} → (x + y) ∼ (y + x)) → (x y : A) → (r : ℤ) → (elementPower G (x + y) r) ∼ (elementPower G x r + elementPower G y r)
+elementPowerHomAbelian ab x y (nonneg n) = positiveEltPowerHomAbelian ab x y n
+elementPowerHomAbelian ab x y (negSucc n) = transitive (transitive (inverseWellDefined G (positiveEltPowerHomAbelian ab x y (succ n))) (inverseWellDefined G ab)) (invContravariant G)
diff --git a/Groups/Lemmas.agda b/Groups/Lemmas.agda
index c40b41d..2f0e157 100644
--- a/Groups/Lemmas.agda
+++ b/Groups/Lemmas.agda
@@ -140,3 +140,6 @@ invContravariant {x} {y} = ans
     otherInvIsInverse = transitive oneMult invRight
     ans : (x · y) ^-1 ∼ (y ^-1) · (x ^-1)
     ans = symmetric (leftInversesAreUnique otherInvIsInverse)
+
+equalsDoubleImpliesZero : {x : A} → (x · x) ∼ x → x ∼ 0G
+equalsDoubleImpliesZero 2x=x = transitive (symmetric identLeft) (transitive (+WellDefined (symmetric invLeft) reflexive) (transitive (symmetric +Associative) (transitive (+WellDefined reflexive 2x=x) invLeft)))
diff --git a/Modules/Definition.agda b/Modules/Definition.agda
new file mode 100644
index 0000000..0f44a54
--- /dev/null
+++ b/Modules/Definition.agda
@@ -0,0 +1,25 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Groups.Abelian.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; _⊔_)
+
+module Modules.Definition {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+R_ _*_) {m n : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} (G : AbelianGroup G') (_·_ : A → M → M) where
+
+record Module : Set (a ⊔ b ⊔ m ⊔ n) where
+  field
+    dotWellDefined : {r s : A} {t u : M} → Setoid._∼_ S r s → Setoid._∼_ T t u → Setoid._∼_ T (r · t) (s · u)
+    dotDistributesLeft : {r : A} {x y : M} → Setoid._∼_ T (r · (x + y)) ((r · x) + (r · y))
+    dotDistributesRight : {r s : A} {x : M} → Setoid._∼_ T ((r +R s) · x) ((r · x) + (s · x))
+    dotAssociative : {r s : A} {x : M} → Setoid._∼_ T ((r * s) · x) (r · (s · x))
+    dotIdentity : {x : M} → Setoid._∼_ T ((Ring.1R R) · x) x
diff --git a/Modules/Examples.agda b/Modules/Examples.agda
new file mode 100644
index 0000000..1dceb40
--- /dev/null
+++ b/Modules/Examples.agda
@@ -0,0 +1,34 @@
+{-# 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 Groups.Abelian.Definition
+open import Numbers.Naturals.Naturals
+open import Numbers.Integers.Integers
+open import Setoids.Orders
+open import Setoids.Setoids
+open import Functions
+open import Sets.EquivalenceRelations
+open import Rings.Definition
+open import Modules.Definition
+open import Groups.Cyclic.Definition
+open import Groups.Cyclic.DefinitionLemmas
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Modules.Examples where
+
+abGrpModule : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {G' : Group S _+_} (G : AbelianGroup G') → Module ℤRing G (λ x i → elementPower G' i x)
+Module.dotWellDefined (abGrpModule {S = S} {G' = G'} G) {m} {n} {g} {h} m=n g=h = transitive (elementPowerWellDefinedG G' g h g=h {m}) (elementPowerWellDefinedZ' G' m n m=n {h})
+  where
+    open Setoid S
+    open Equivalence eq
+Module.dotDistributesLeft (abGrpModule {G' = G'} G) {n} {x} {y} = elementPowerHomAbelian G' (AbelianGroup.commutative G) x y n
+Module.dotDistributesRight (abGrpModule {S = S} {G' = G'} G) {r} {s} {x} = symmetric (elementPowerCollapse G' x r s)
+  where
+    open Equivalence (Setoid.eq S)
+Module.dotAssociative (abGrpModule {G' = G'} G) {r} {s} {x} = elementPowerMultiplies G' r s x
+Module.dotIdentity (abGrpModule {G' = G'} G) = Group.identRight G'
diff --git a/Modules/Lemmas.agda b/Modules/Lemmas.agda
new file mode 100644
index 0000000..e4a5433
--- /dev/null
+++ b/Modules/Lemmas.agda
@@ -0,0 +1,39 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+open import Groups.Groups
+open import Groups.Homomorphisms.Definition
+open import Groups.Definition
+open import Groups.Lemmas
+open import Groups.Abelian.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 Modules.Definition
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module Modules.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+R_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+R_ _*_} {m n : _} {M : Set m} {T : Setoid {m} {n} M} {_+_ : M → M → M} {G' : Group T _+_} {G : AbelianGroup G'} {_·_ : A → M → M} (mod : Module R G _·_) where
+
+open Group G'
+open Ring R
+open Setoid T
+open Equivalence eq
+open Module mod
+
+moduleTimesZero : {x : M} → (0R · x) ∼ 0G
+moduleTimesZero {x} = equalsDoubleImpliesZero G' (symmetric x=2x)
+  where
+    x=2x : (0R · x) ∼ (0R · x) + (0R · x)
+    x=2x = transitive (dotWellDefined (Equivalence.symmetric (Setoid.eq S) (Group.identLeft additiveGroup)) reflexive) dotDistributesRight
+
+moduleTimes-1 : {x : M} → ((Group.inverse additiveGroup 1R) · x) ∼ inverse x
+moduleTimes-1 {x} = transitive (transferToRight' G' j) (inverseWellDefined G' dotIdentity)
+  where
+    i : ((1R · x) + ((Group.inverse additiveGroup 1R) · x)) ∼ 0G
+    i = transitive (symmetric (transitive (dotWellDefined (Equivalence.symmetric (Setoid.eq S) (Group.invRight additiveGroup {1R})) reflexive) dotDistributesRight)) (moduleTimesZero)
+    j : (((Group.inverse additiveGroup 1R) · x) + (1R · x)) ∼ 0G
+    j = transitive (AbelianGroup.commutative G) i