diff --git a/CHANGELOG.md b/CHANGELOG.md
index 03ff70d81e..b3e78bf920 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -193,34 +193,31 @@ New modules
   `Data.Unit.Polymorphic.Instances`, `Data.Vec.Instances`,
   `Data.Word.Instances`, and `Reflection.Instances`.
 
-* Generic divisibility over algebraic structures
+* Generic definitions over algebraic structures (divisibility, multiplication etc.):
   ```
-  Algebra.Divisibility
-  Algebra.GCD
-  Algebra.Primality
-  Algebra.Properties.Magma.Divisibility
-  Algebra.Properties.Semigroup.Divisibility
-  Algebra.Properties.Monoid.Divisibility
-  Algebra.Properties.CommutativeSemigroup.Divisibility
-  Algebra.Properties.Semiring.Divisibility
-  Algebra.Properties.Semiring.GCD
+  Algebra.Definitions.RawMagma
+  Algebra.Definitions.RawMonoid
+  Algebra.Definitions.RawSemiring
   ```
 
-* Generic summation over algebraic structures
+* Properties of generic definitions over algebraic structures (divisibility, multiplication etc.):
   ```
+  Algebra.Properties.Magma.Divisibility
+  
+  Algebra.Properties.Semigroup.Divisibility
+  
+  Algebra.Properties.CommutativeSemigroup.Divisibility
+  
   Algebra.Properties.Monoid.Summation
-  Algebra.Properties.CommutativeMonoid.Summation
-  ```
-
-* Generic multiplication over algebraic structures
-  ```
   Algebra.Properties.Monoid.Multiplication
+  Algebra.Properties.Monoid.Divisibility
+  
+  Algebra.Properties.CommutativeMonoid.Summation
+  
   Algebra.Properties.Semiring.Multiplication
-  ```
-
-* Generic exponentiation over algebraic structures
-  ```
   Algebra.Properties.Semiring.Exponentiation
+  Algebra.Properties.Semiring.GCD
+  Algebra.Properties.Semiring.Divisibility
   ```
 
 * Setoid equality over vectors:
diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
index 797a9b3583..7b911768ad 100644
--- a/src/Algebra/Bundles.agda
+++ b/src/Algebra/Bundles.agda
@@ -15,6 +15,7 @@ open import Algebra.Core
 open import Algebra.Structures
 open import Relation.Binary
 open import Function.Base
+import Relation.Nullary as N
 open import Level
 
 ------------------------------------------------------------------------
@@ -29,6 +30,10 @@ record RawMagma c ℓ : Set (suc (c ⊔ ℓ)) where
     _≈_     : Rel Carrier ℓ
     _∙_     : Op₂ Carrier
 
+  infix 4 _≉_
+  _≉_ : Rel Carrier _
+  x ≉ y = N.¬ (x ≈ y)
+
 
 record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -44,7 +49,7 @@ record Magma c ℓ : Set (suc (c ⊔ ℓ)) where
   rawMagma : RawMagma _ _
   rawMagma = record { _≈_ = _≈_; _∙_ = _∙_ }
 
-  open Setoid setoid public
+  open RawMagma rawMagma public
     using (_≉_)
 
 
@@ -178,6 +183,9 @@ record RawMonoid c ℓ : Set (suc (c ⊔ ℓ)) where
     ; _∙_ = _∙_
     }
 
+  open RawMagma rawMagma public
+    using (_≉_)
+
 
 record Monoid c ℓ : Set (suc (c ⊔ ℓ)) where
   infixl 7 _∙_
@@ -281,7 +289,7 @@ record RawGroup c ℓ : Set (suc (c ⊔ ℓ)) where
     }
 
   open RawMonoid rawMonoid public
-    using (rawMagma)
+    using (_≉_; rawMagma)
 
 
 record Group c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -354,6 +362,9 @@ record RawLattice c ℓ : Set (suc (c ⊔ ℓ)) where
   ∧-rawMagma : RawMagma c ℓ
   ∧-rawMagma = record { _≈_ = _≈_; _∙_ = _∧_ }
 
+  open RawMagma ∨-rawMagma public
+    using (_≉_)
+
 
 record Lattice c ℓ : Set (suc (c ⊔ ℓ)) where
   infixr 7 _∧_
@@ -428,7 +439,7 @@ record RawNearSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     }
 
   open RawMonoid +-rawMonoid public
-    using () renaming (rawMagma to +-rawMagma)
+    using (_≉_) renaming (rawMagma to +-rawMagma)
 
   *-rawMagma : RawMagma c ℓ
   *-rawMagma = record
@@ -568,7 +579,7 @@ record RawSemiring c ℓ : Set (suc (c ⊔ ℓ)) where
     }
 
   open RawNearSemiring rawNearSemiring public
-    using (+-rawMonoid; +-rawMagma; *-rawMagma)
+    using (_≉_; +-rawMonoid; +-rawMagma; *-rawMagma)
 
   *-rawMonoid : RawMonoid c ℓ
   *-rawMonoid = record
diff --git a/src/Algebra/Divisibility.agda b/src/Algebra/Definitions/RawMagma.agda
similarity index 52%
rename from src/Algebra/Divisibility.agda
rename to src/Algebra/Definitions/RawMagma.agda
index 8db709a258..25f03cb6e9 100644
--- a/src/Algebra/Divisibility.agda
+++ b/src/Algebra/Definitions/RawMagma.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Definition of divisibility
+-- Basic auxiliary definitions for magma-like structures
 ------------------------------------------------------------------------
 
 -- You're unlikely to want to use this module directly. Instead you
@@ -10,16 +10,17 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Algebra.Core
+open import Algebra.Bundles using (RawMagma)
 open import Data.Product using (∃; _×_; _,_)
 open import Level using (_⊔_)
 open import Relation.Binary
 open import Relation.Nullary using (¬_)
 
-module Algebra.Divisibility
-  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_∙_ : Op₂ A)
+module Algebra.Definitions.RawMagma
+  {a ℓ} (M : RawMagma a ℓ)
   where
 
+open RawMagma M renaming (Carrier to A)
 open import Algebra.Definitions _≈_
 
 ------------------------------------------------------------------------
@@ -65,35 +66,3 @@ x ∣∣ y = x ∣ y × y ∣ x
 
 _∤∤_ : Rel A (a ⊔ ℓ)
 x ∤∤ y =  ¬ x ∣∣ y
-
-------------------------------------------------------------------------------
--- Greatest common divisor (GCD)
-
-record IsGCD (x y gcd : A) : Set (a ⊔ ℓ) where
-  constructor gcdᶜ
-  field
-    divides₁ : gcd ∣ x
-    divides₂ : gcd ∣ y
-    greatest : ∀ {z} → z ∣ x → z ∣ y → z ∣ gcd
-
-------------------------------------------------------------------------
--- Properties
-
-∣-refl : ∀ {ε} → LeftIdentity ε _∙_ → Reflexive _∣_
-∣-refl {ε} idˡ {x} = ε , idˡ x
-
-∣-reflexive : Transitive _≈_ → ∀ {ε} → LeftIdentity ε _∙_ → _≈_ ⇒ _∣_
-∣-reflexive trans {ε} idˡ x≈y = ε , trans (idˡ _) x≈y
-
-∣-trans : Transitive _≈_ → LeftCongruent _∙_ → Associative _∙_ → Transitive _∣_
-∣-trans trans congˡ assoc {x} {y} {z} (p , px≈y) (q , qy≈z) =
-  q ∙ p , trans (assoc q p x) (trans (congˡ px≈y) qy≈z)
-
-∣-respʳ : Transitive _≈_ → _∣_ Respectsʳ _≈_
-∣-respʳ trans y≈z (q , qx≈y) = q , trans qx≈y y≈z
-
-∣-respˡ : Symmetric _≈_ → Transitive _≈_ → LeftCongruent _∙_ → _∣_ Respectsˡ _≈_
-∣-respˡ sym trans congˡ x≈z (q , qx≈y) = q , trans (congˡ (sym x≈z)) qx≈y
-
-∣-resp : Symmetric _≈_ → Transitive _≈_ → LeftCongruent _∙_ → _∣_ Respects₂ _≈_
-∣-resp sym trans cong = ∣-respʳ trans , ∣-respˡ sym trans cong
diff --git a/src/Algebra/Definitions/RawMonoid.agda b/src/Algebra/Definitions/RawMonoid.agda
new file mode 100644
index 0000000000..b1b488d85f
--- /dev/null
+++ b/src/Algebra/Definitions/RawMonoid.agda
@@ -0,0 +1,65 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Basic auxiliary definitions for monoid-like structures
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (RawMonoid)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Vec.Functional as Vector using (Vector)
+
+module Algebra.Definitions.RawMonoid {a ℓ} (M : RawMonoid a ℓ) where
+
+open RawMonoid M renaming ( _∙_ to _+_ ; ε to 0# )
+
+------------------------------------------------------------------------
+-- Re-export definitions over a magma
+------------------------------------------------------------------------
+
+open import Algebra.Definitions.RawMagma rawMagma public
+
+------------------------------------------------------------------------
+-- Multiplication by natural number
+------------------------------------------------------------------------
+-- Standard definition
+
+-- A simple definition, easy to use and prove properties about.
+
+infixr 8 _×_
+
+_×_ : ℕ → Carrier → Carrier
+0     × x = 0#
+suc n × x = x + (n × x)
+
+------------------------------------------------------------------------
+-- Type-checking optimised definition
+
+-- For use in code where high performance at type-checking time is
+-- important, e.g. solvers and tactics. Firstly it avoids unnecessarily
+-- multiplying by the unit if possible, speeding up type-checking and
+-- makes for much more readable proofs:
+--
+--     Standard definition:  x * 2 = x + x + 0#
+--     Optimised definition: x * 2 = x + x
+--
+-- Secondly, associates to the left which, counterintuitive as it may
+-- seem, also speeds up typechecking.
+--
+--     Standard definition: x * 3 = x + (x + (x + 0#))
+--     Our definition:      x * 3 = (x + x) + x
+
+infixl 8 _×′_
+
+_×′_ : ℕ → Carrier → Carrier
+0     ×′ x = 0#
+1     ×′ x = x
+suc n ×′ x = x + n ×′ x
+
+------------------------------------------------------------------------
+-- Summation
+------------------------------------------------------------------------
+
+sum : ∀ {n} → Vector Carrier n → Carrier
+sum = Vector.foldr _+_ 0#
diff --git a/src/Algebra/Definitions/RawSemiring.agda b/src/Algebra/Definitions/RawSemiring.agda
new file mode 100644
index 0000000000..20d29831bb
--- /dev/null
+++ b/src/Algebra/Definitions/RawSemiring.agda
@@ -0,0 +1,67 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Basic auxiliary definitions for semiring-like structures
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (RawSemiring)
+open import Data.Sum.Base using (_⊎_)
+open import Level using (_⊔_)
+open import Relation.Binary.Core using (Rel)
+
+module Algebra.Definitions.RawSemiring {a ℓ} (M : RawSemiring a ℓ) where
+
+open RawSemiring M renaming (Carrier to A)
+
+------------------------------------------------------------------------
+-- Definitions over _+_
+
+open import Algebra.Definitions.RawMonoid +-rawMonoid public
+  using
+  ( _×_
+  ; _×′_
+  ; sum
+  )
+
+------------------------------------------------------------------------
+-- Definitions over _*_
+
+open import Algebra.Definitions.RawMonoid *-rawMonoid public
+  using
+  ( _∣_
+  ; _∤_
+  )
+  renaming
+  ( sum to product
+  )
+
+------------------------------------------------------------------------
+-- Coprimality
+
+Coprime : Rel A (a ⊔ ℓ)
+Coprime x y = ∀ {z} → z ∣ x → z ∣ y → z ∣ 1#
+
+record Irreducible (p : A) : Set (a ⊔ ℓ) where
+  constructor mkIrred
+  field
+    p∤1       : p ∤ 1#
+    split-∣1 : ∀ {x y} → p ≈ (x * y) → x ∣ 1# ⊎ y ∣ 1#
+
+record Prime (p : A) : Set (a ⊔ ℓ) where
+  constructor mkPrime
+  field
+    p≉0     : p ≉ 0#
+    split-∣ : ∀ {x y} → p ∣ x * y → p ∣ x ⊎ p ∣ y
+
+------------------------------------------------------------------------
+-- Greatest common divisor
+
+record IsGCD (x y gcd : A) : Set (a ⊔ ℓ) where
+  constructor gcdᶜ
+  field
+    divides₁ : gcd ∣ x
+    divides₂ : gcd ∣ y
+    greatest : ∀ {z} → z ∣ x → z ∣ y → z ∣ gcd
+
diff --git a/src/Algebra/Operations/CommutativeMonoid.agda b/src/Algebra/Operations/CommutativeMonoid.agda
index b652fda938..98ca20255d 100644
--- a/src/Algebra/Operations/CommutativeMonoid.agda
+++ b/src/Algebra/Operations/CommutativeMonoid.agda
@@ -13,7 +13,9 @@ open import Algebra
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.Fin.Base using (Fin; zero)
 open import Data.Table.Base as Table using (Table)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Function.Base using (_∘_)
+open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 module Algebra.Operations.CommutativeMonoid
@@ -22,15 +24,22 @@ module Algebra.Operations.CommutativeMonoid
 
 {-# WARNING_ON_IMPORT
 "Algebra.Operations.CommutativeMonoid was deprecated in v1.5.
-Use Algebra.Properties.CommutativeMonoid.(Summation/Multiplication) instead."
+Use Algebra.Properties.CommutativeMonoid.(Summation/Multiplication/Multiplication.TCOptimised) instead."
 #-}
 
 open CommutativeMonoid CM
   renaming
   ( _∙_       to _+_
   ; ε         to 0#
+  ; identityʳ to +-identityʳ
+  ; identityˡ to +-identityˡ
+  ; ∙-cong    to +-cong
+  ; ∙-congˡ   to +-congˡ
+  ; assoc     to +-assoc
   )
 
+open import Relation.Binary.Reasoning.Setoid setoid
+
 -- Summation over lists/tables
 
 sumₗ : List Carrier → Carrier
@@ -49,6 +58,69 @@ sumₜ-syntax _ = sumₜ ∘ Table.tabulate
 syntax sumₜ-syntax n (λ i → x) = ∑[ i < n ] x
 
 ------------------------------------------------------------------------
--- Operations
+-- Multiplication
+
+infixr 8 _×_ _×′_
+
+_×_ : ℕ → Carrier → Carrier
+0     × x = 0#
+suc n × x = x + (n × x)
+
+_×′_ : ℕ → Carrier → Carrier
+0     ×′ x = 0#
+1     ×′ x = x
+suc n ×′ x = x + n ×′ x
+
+------------------------------------------------------------------------
+-- Properties of _×_
+
+×-congʳ : ∀ n → (n ×_) Preserves _≈_ ⟶ _≈_
+×-congʳ 0       x≈x′ = refl
+×-congʳ (suc n) x≈x′ = +-cong x≈x′ (×-congʳ n x≈x′)
+
+×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
+×-cong {u} P.refl x≈x′ = ×-congʳ u x≈x′
+
+-- _×_ is homomorphic with respect to _ℕ+_/_+_.
+
+×-homo-+ : ∀ c m n → (m ℕ.+ n) × c ≈ m × c + n × c
+×-homo-+ c 0       n = sym (+-identityˡ (n × c))
+×-homo-+ c (suc m) n = begin
+  c + (m ℕ.+ n) × c    ≈⟨ +-cong refl (×-homo-+ c m n) ⟩
+  c + (m × c + n × c)  ≈⟨ sym (+-assoc c (m × c) (n × c)) ⟩
+  c + m × c + n × c    ∎
+
+------------------------------------------------------------------------
+-- Properties of _×′_
+
+1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x
+1+×′ 0       x = sym (+-identityʳ x)
+1+×′ (suc n) x = refl
+
+-- _×_ and _×′_ are extensionally equal (up to the setoid
+-- equivalence).
+
+×≈×′ : ∀ n x → n × x ≈ n ×′ x
+×≈×′ 0       x = refl
+×≈×′ (suc n) x = begin
+  x + n × x   ≈⟨ +-congˡ (×≈×′ n x) ⟩
+  x + n ×′ x  ≈⟨ sym (1+×′ n x) ⟩
+  suc n ×′ x  ∎
+
+-- _×′_ is homomorphic with respect to _ℕ+_/_+_.
+
+×′-homo-+ : ∀ c m n → (m ℕ.+ n) ×′ c ≈ m ×′ c + n ×′ c
+×′-homo-+ c m n = begin
+  (m ℕ.+ n) ×′ c   ≈⟨ sym (×≈×′ (m ℕ.+ n) c) ⟩
+  (m ℕ.+ n) ×  c   ≈⟨ ×-homo-+ c m n ⟩
+  m ×  c + n ×  c  ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩
+  m ×′ c + n ×′ c  ∎
+
+-- _×′_ preserves equality.
 
-open import Algebra.Properties.Monoid.Multiplication monoid public
+×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
+×′-cong {n} {_} {x} {y} P.refl x≈y = begin
+  n  ×′ x ≈⟨ sym (×≈×′ n x) ⟩
+  n  ×  x ≈⟨ ×-congʳ n x≈y ⟩
+  n  ×  y ≈⟨ ×≈×′ n y ⟩
+  n  ×′ y ∎
diff --git a/src/Algebra/Primality.agda b/src/Algebra/Primality.agda
deleted file mode 100644
index 9661776da8..0000000000
--- a/src/Algebra/Primality.agda
+++ /dev/null
@@ -1,42 +0,0 @@
-------------------------------------------------------------------------
--- The Agda standard library
---
--- Definitions of irreducibility, primality, coprimality.
-------------------------------------------------------------------------
-
--- You're unlikely to want to use this module directly. Instead you
--- probably want to be importing the appropriate module from e.g.
--- `Algebra.Properties.Semiring.Primality`.
-
-{-# OPTIONS --without-K --safe #-}
-
-open import Algebra.Core using (Op₂)
-open import Data.Sum using (_⊎_)
-open import Function using (flip)
-open import Level using (_⊔_)
-open import Relation.Binary using (Rel; Symmetric)
-open import Relation.Nullary using (¬_)
-
-module Algebra.Primality
-  {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) (_*_ : Op₂ A) (0# 1# : A)
-  where
-
-open import Algebra.Divisibility _≈_ _*_
-
-------------------------------------------------------------------------------
--- Definitions
-
-Coprime : Rel A (a ⊔ ℓ)
-Coprime x y = ∀ {z} → z ∣ x → z ∣ y → z ∣ 1#
-
-record Irreducible (p : A) : Set (a ⊔ ℓ) where
-  constructor mkIrred
-  field
-    p∤1       : p ∤ 1#
-    split-∣1 : ∀ {x y} → p ≈ (x * y) → x ∣ 1# ⊎ y ∣ 1#
-
-record Prime (p : A) : Set (a ⊔ ℓ) where
-  constructor mkPrime
-  field
-    p≉0     : ¬ (p ≈ 0#)
-    split-∣ : ∀ {x y} → p ∣ x * y → p ∣ x ⊎ p ∣ y
diff --git a/src/Algebra/Properties/Magma/Divisibility.agda b/src/Algebra/Properties/Magma/Divisibility.agda
index 86e59afb05..50cf0bf172 100644
--- a/src/Algebra/Properties/Magma/Divisibility.agda
+++ b/src/Algebra/Properties/Magma/Divisibility.agda
@@ -17,20 +17,20 @@ open Magma M
 ------------------------------------------------------------------------
 -- Re-export divisibility relations publicly
 
-open import Algebra.Divisibility _≈_ _∙_ as Div public
+open import Algebra.Definitions.RawMagma rawMagma public
   using (_∣_; _∤_; _∣∣_; _∤∤_)
 
 ------------------------------------------------------------------------
 -- Properties of divisibility
 
 ∣-respʳ : _∣_ Respectsʳ _≈_
-∣-respʳ = Div.∣-respʳ trans
+∣-respʳ y≈z (q , qx≈y) = q , trans qx≈y y≈z
 
 ∣-respˡ : _∣_ Respectsˡ _≈_
-∣-respˡ = Div.∣-respˡ sym trans ∙-congˡ
+∣-respˡ x≈z (q , qx≈y) = q , trans (∙-congˡ (sym x≈z)) qx≈y
 
 ∣-resp : _∣_ Respects₂ _≈_
-∣-resp = Div.∣-resp sym trans ∙-congˡ
+∣-resp = ∣-respʳ , ∣-respˡ
 
 x∣yx : ∀ x y → x ∣ y ∙ x
 x∣yx x y = y , refl
diff --git a/src/Algebra/Properties/Monoid/Divisibility.agda b/src/Algebra/Properties/Monoid/Divisibility.agda
index 618d2c4923..bc970f8a02 100644
--- a/src/Algebra/Properties/Monoid/Divisibility.agda
+++ b/src/Algebra/Properties/Monoid/Divisibility.agda
@@ -7,15 +7,13 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra using (Monoid)
-import Algebra.Properties.Semigroup
-open import Level using (_⊔_)
 open import Data.Product using (_,_)
 open import Relation.Binary
 
-module Algebra.Properties.Monoid.Divisibility {a ℓ} (M : Monoid a ℓ) where
+module Algebra.Properties.Monoid.Divisibility
+  {a ℓ} (M : Monoid a ℓ) where
 
 open Monoid M
-import Algebra.Divisibility _≈_ _∙_ as Div
 
 ------------------------------------------------------------------------
 -- Re-export semigroup divisibility
@@ -29,10 +27,10 @@ open import Algebra.Properties.Semigroup.Divisibility semigroup public
 ε∣ x = x , identityʳ x
 
 ∣-refl : Reflexive _∣_
-∣-refl = Div.∣-refl identityˡ
+∣-refl {x} = ε , identityˡ x
 
 ∣-reflexive : _≈_ ⇒ _∣_
-∣-reflexive = Div.∣-reflexive trans identityˡ
+∣-reflexive x≈y = ε , trans (identityˡ _) x≈y
 
 ∣-isPreorder : IsPreorder _≈_ _∣_
 ∣-isPreorder = record
@@ -41,7 +39,7 @@ open import Algebra.Properties.Semigroup.Divisibility semigroup public
   ; trans         = ∣-trans
   }
 
-∣-preorder : Preorder a ℓ (a ⊔ ℓ)
+∣-preorder : Preorder a ℓ _
 ∣-preorder = record
   { isPreorder = ∣-isPreorder
   }
diff --git a/src/Algebra/Properties/Monoid/Multiplication.agda b/src/Algebra/Properties/Monoid/Multiplication.agda
index 4818668395..426e4127fe 100644
--- a/src/Algebra/Properties/Monoid/Multiplication.agda
+++ b/src/Algebra/Properties/Monoid/Multiplication.agda
@@ -13,7 +13,7 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 module Algebra.Properties.Monoid.Multiplication {a ℓ} (M : Monoid a ℓ) where
 
--- View of the monoid operator as an addition
+-- View of the monoid operator as addition
 open Monoid M
   renaming
   ( _∙_       to _+_
@@ -24,27 +24,16 @@ open Monoid M
   ; assoc     to +-assoc
   ; ε         to 0#
   )
+
 open import Relation.Binary.Reasoning.Setoid setoid
+
 open import Algebra.Definitions _≈_
 
 ------------------------------------------------------------------------
 -- Definition
 
--- Multiplication by natural number.
-
-infixr 8 _×_ _×′_
-
-_×_ : ℕ → Carrier → Carrier
-0     × x = 0#
-suc n × x = x + (n × x)
-
--- A variant that includes a "redundant" case which ensures that `1 × x`
--- is definitionally equal to `x`.
-
-_×′_ : ℕ → Carrier → Carrier
-0     ×′ x = 0#
-1     ×′ x = x
-suc n ×′ x = x + n ×′ x
+open import Algebra.Definitions.RawMonoid rawMonoid public
+  using (_×_)
 
 ------------------------------------------------------------------------
 -- Properties of _×_
@@ -72,38 +61,3 @@ suc n ×′ x = x + n ×′ x
   c + (suc n × c) ≈⟨ +-congˡ (×-idem idem (suc n) ) ⟩
   c + c           ≈⟨ idem ⟩
   c               ∎
-
-------------------------------------------------------------------------
--- Properties of _×′_
-
-1+×′ : ∀ n x → suc n ×′ x ≈ x + n ×′ x
-1+×′ 0       x = sym (+-identityʳ x)
-1+×′ (suc n) x = refl
-
--- _×_ and _×′_ are extensionally equal (up to the setoid
--- equivalence).
-
-×≈×′ : ∀ n x → n × x ≈ n ×′ x
-×≈×′ 0       x = refl
-×≈×′ (suc n) x = begin
-  x + n × x   ≈⟨ +-congˡ (×≈×′ n x) ⟩
-  x + n ×′ x  ≈⟨ sym (1+×′ n x) ⟩
-  suc n ×′ x  ∎
-
--- _×′_ is homomorphic with respect to _ℕ+_/_+_.
-
-×′-homo-+ : ∀ c m n → (m ℕ.+ n) ×′ c ≈ m ×′ c + n ×′ c
-×′-homo-+ c m n = begin
-  (m ℕ.+ n) ×′ c   ≈⟨ sym (×≈×′ (m ℕ.+ n) c) ⟩
-  (m ℕ.+ n) ×  c   ≈⟨ ×-homo-+ c m n ⟩
-  m ×  c + n ×  c  ≈⟨ +-cong (×≈×′ m c) (×≈×′ n c) ⟩
-  m ×′ c + n ×′ c  ∎
-
--- _×′_ preserves equality.
-
-×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
-×′-cong {n} {_} {x} {y} P.refl x≈y = begin
-  n  ×′ x ≈⟨ sym (×≈×′ n x) ⟩
-  n  ×  x ≈⟨ ×-congʳ n x≈y ⟩
-  n  ×  y ≈⟨ ×≈×′ n y ⟩
-  n  ×′ y ∎
diff --git a/src/Algebra/Properties/Monoid/Multiplication/TCOptimised.agda b/src/Algebra/Properties/Monoid/Multiplication/TCOptimised.agda
new file mode 100644
index 0000000000..4c6fee8056
--- /dev/null
+++ b/src/Algebra/Properties/Monoid/Multiplication/TCOptimised.agda
@@ -0,0 +1,72 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Multiplication over a monoid (i.e. repeated addition) optimised for
+-- type checking.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles using (Monoid)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Relation.Binary.Core using (_Preserves₂_⟶_⟶_)
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+module Algebra.Properties.Monoid.Multiplication.TCOptimised
+  {a ℓ} (M : Monoid a ℓ) where
+
+open Monoid M renaming
+  ( _∙_       to _+_
+  ; ∙-cong    to +-cong
+  ; ∙-congˡ   to +-congˡ
+  ; identityˡ to +-identityˡ
+  ; identityʳ to +-identityʳ
+  ; assoc     to +-assoc
+  ; ε         to 0#
+  )
+
+open import Algebra.Properties.Monoid.Multiplication M as U
+  using () renaming (_×_ to _×ᵤ_)
+
+open import Relation.Binary.Reasoning.Setoid setoid
+
+------------------------------------------------------------------------
+-- Definition
+
+open import Algebra.Definitions.RawMonoid rawMonoid public
+  using () renaming (_×′_ to _×_)
+
+------------------------------------------------------------------------
+-- Properties of _×′_
+
+1+× : ∀ n x → suc n × x ≈ x + n × x
+1+× 0       x = sym (+-identityʳ x)
+1+× (suc n) x = refl
+
+-- The unoptimised (_×ᵤ_) and optimised (_×_) versions of multiplication
+-- are extensionally equal (up to the setoid equivalence).
+
+×ᵤ≈× : ∀ n x → n ×ᵤ x ≈ n × x
+×ᵤ≈× 0       x = refl
+×ᵤ≈× (suc n) x = begin
+  x + n ×ᵤ x  ≈⟨ +-congˡ (×ᵤ≈× n x) ⟩
+  x + n ×  x  ≈˘⟨ 1+× n x ⟩
+  suc n ×  x  ∎
+
+-- _×_ is homomorphic with respect to _ℕ.+_/_+_.
+
+×-homo-+ : ∀ c m n → (m ℕ.+ n) × c ≈ m × c + n × c
+×-homo-+ c m n = begin
+  (m ℕ.+ n) ×  c   ≈˘⟨ ×ᵤ≈× (m ℕ.+ n) c ⟩
+  (m ℕ.+ n) ×ᵤ c   ≈⟨ U.×-homo-+ c m n ⟩
+  m ×ᵤ c + n ×ᵤ c  ≈⟨ +-cong (×ᵤ≈× m c) (×ᵤ≈× n c) ⟩
+  m ×  c + n ×  c  ∎
+
+-- _×_ preserves equality.
+
+×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
+×-cong {n} {_} {x} {y} P.refl x≈y = begin
+  n  ×  x ≈˘⟨ ×ᵤ≈× n x ⟩
+  n  ×ᵤ x ≈⟨  U.×-congʳ n x≈y ⟩
+  n  ×ᵤ y ≈⟨  ×ᵤ≈× n y ⟩
+  n  ×  y ∎
diff --git a/src/Algebra/Properties/Monoid/Summation.agda b/src/Algebra/Properties/Monoid/Summation.agda
index aac92997e2..808270681d 100644
--- a/src/Algebra/Properties/Monoid/Summation.agda
+++ b/src/Algebra/Properties/Monoid/Summation.agda
@@ -35,8 +35,8 @@ open import Algebra.Definitions _≈_
 ------------------------------------------------------------------------
 -- Definition
 
-sum : ∀ {n} → Vector Carrier n → Carrier
-sum = Vector.foldr _+_ 0#
+open import Algebra.Definitions.RawMonoid rawMonoid public
+  using (sum)
 
 ------------------------------------------------------------------------
 -- An alternative mathematical-style syntax for sumₜ
diff --git a/src/Algebra/Properties/Semigroup/Divisibility.agda b/src/Algebra/Properties/Semigroup/Divisibility.agda
index 7ab07d91f5..755131f03a 100644
--- a/src/Algebra/Properties/Semigroup/Divisibility.agda
+++ b/src/Algebra/Properties/Semigroup/Divisibility.agda
@@ -7,12 +7,13 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra using (Semigroup)
+open import Data.Product using (_,_)
 open import Relation.Binary.Definitions using (Transitive)
 
-module Algebra.Properties.Semigroup.Divisibility {a ℓ} (S : Semigroup a ℓ) where
+module Algebra.Properties.Semigroup.Divisibility
+  {a ℓ} (S : Semigroup a ℓ) where
 
 open Semigroup S
-import Algebra.Divisibility _≈_ _∙_ as Div
 
 ------------------------------------------------------------------------
 -- Re-export magma divisibility
@@ -23,4 +24,5 @@ open import Algebra.Properties.Magma.Divisibility magma public
 -- Additional properties
 
 ∣-trans : Transitive _∣_
-∣-trans = Div.∣-trans trans ∙-congˡ assoc
+∣-trans (p , px≈y) (q , qy≈z) =
+  q ∙ p , trans (assoc q p _) (trans (∙-congˡ px≈y) qy≈z)
diff --git a/src/Algebra/Properties/Semiring/GCD.agda b/src/Algebra/Properties/Semiring/GCD.agda
index fccd46ec83..832454eb27 100644
--- a/src/Algebra/Properties/Semiring/GCD.agda
+++ b/src/Algebra/Properties/Semiring/GCD.agda
@@ -19,7 +19,7 @@ open import Algebra.Properties.Semiring.Divisibility R
 ------------------------------------------------------------------------
 -- Re-exporting definition of GCD
 
-open import Algebra.Divisibility _≈_ _*_ public
+open import Algebra.Definitions.RawSemiring rawSemiring public
   using (IsGCD; gcdᶜ)
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Properties/Semiring/Multiplication.agda b/src/Algebra/Properties/Semiring/Multiplication.agda
index 2c9ad7b8b0..ecd56613f4 100644
--- a/src/Algebra/Properties/Semiring/Multiplication.agda
+++ b/src/Algebra/Properties/Semiring/Multiplication.agda
@@ -7,7 +7,6 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra
-import Algebra.Properties.Monoid.Multiplication as MonoidMultiplication
 open import Data.Nat.Base as ℕ using (zero; suc)
 
 module Algebra.Properties.Semiring.Multiplication
@@ -19,7 +18,7 @@ open import Relation.Binary.Reasoning.Setoid setoid
 ------------------------------------------------------------------------
 -- Re-export definition from the monoid
 
-open MonoidMultiplication +-monoid public
+open import Algebra.Properties.Monoid.Multiplication +-monoid public
 
 ------------------------------------------------------------------------
 -- Properties of _×_
@@ -34,15 +33,3 @@ open MonoidMultiplication +-monoid public
   n × 1# + (m × 1#) * (n × 1#)        ≈˘⟨ +-congʳ (*-identityˡ _) ⟩
   1# * (n × 1#) + (m × 1#) * (n × 1#) ≈˘⟨ distribʳ (n × 1#) 1# (m × 1#) ⟩
   (1# + m × 1#) * (n × 1#)            ∎
-
-------------------------------------------------------------------------
--- Properties of _×′_
-
--- (_×′ 1#) is homomorphic with respect to _ℕ.*_/_*_.
-
-×′1-homo-* : ∀ m n → (m ℕ.* n) ×′ 1# ≈ (m ×′ 1#) * (n ×′ 1#)
-×′1-homo-* m n = begin
-  (m ℕ.* n) ×′ 1#        ≈˘⟨ ×≈×′ (m ℕ.* n) 1# ⟩
-  (m ℕ.* n) ×  1#        ≈⟨  ×1-homo-* m n ⟩
-  (m ×  1#) * (n ×  1#)  ≈⟨  *-cong (×≈×′ m 1#) (×≈×′ n 1#) ⟩
-  (m ×′ 1#) * (n ×′ 1#)  ∎
diff --git a/src/Algebra/Properties/Semiring/Multiplication/TCOptimised.agda b/src/Algebra/Properties/Semiring/Multiplication/TCOptimised.agda
new file mode 100644
index 0000000000..90967b4bd0
--- /dev/null
+++ b/src/Algebra/Properties/Semiring/Multiplication/TCOptimised.agda
@@ -0,0 +1,36 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Optimised multiplication by a natural number over a semiring
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra
+open import Data.Nat.Base as ℕ using (zero; suc)
+
+module Algebra.Properties.Semiring.Multiplication.TCOptimised
+  {a ℓ} (S : Semiring a ℓ) where
+
+open Semiring S renaming (zero to *-zero)
+open import Relation.Binary.Reasoning.Setoid setoid
+
+open import Algebra.Properties.Semiring.Multiplication S as U
+  using () renaming (_×_ to _×ᵤ_)
+
+------------------------------------------------------------------------
+-- Re-export definition from the monoid
+
+open import Algebra.Properties.Monoid.Multiplication.TCOptimised +-monoid public
+
+------------------------------------------------------------------------
+-- Properties of _×_
+
+-- (_×′ 1#) is homomorphic with respect to _ℕ.*_/_*_.
+
+×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#)
+×1-homo-* m n = begin
+  (m ℕ.* n) ×  1#        ≈˘⟨ ×ᵤ≈× (m ℕ.* n) 1# ⟩
+  (m ℕ.* n) ×ᵤ 1#        ≈⟨  U.×1-homo-* m n ⟩
+  (m ×ᵤ 1#) * (n ×ᵤ 1#)  ≈⟨  *-cong (×ᵤ≈× m 1#) (×ᵤ≈× n 1#) ⟩
+  (m ×  1#) * (n ×  1#)  ∎
diff --git a/src/Algebra/Properties/Semiring/Primality.agda b/src/Algebra/Properties/Semiring/Primality.agda
index 8ad224c6b1..f8f88a40c7 100644
--- a/src/Algebra/Properties/Semiring/Primality.agda
+++ b/src/Algebra/Properties/Semiring/Primality.agda
@@ -7,34 +7,22 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Algebra using (Semiring)
-import Algebra.Primality
-import Algebra.Properties.Semigroup.Divisibility as SemigroupDiv
-import Algebra.Properties.Semiring.Divisibility as SemiringDiv
-open import Data.Product using (_×_; _,_; proj₁; proj₂)
-open import Data.Sum using (_⊎_; inj₁; inj₂; reduce)
-open import Function using (case_of_; flip)
-open import Level using (_⊔_)
-open import Relation.Binary using (Rel; Symmetric; Setoid)
-open import Relation.Unary using (Pred)
+open import Data.Sum.Base using (reduce)
+open import Function.Base using (flip)
+open import Relation.Binary using (Symmetric)
 
 module Algebra.Properties.Semiring.Primality
   {a ℓ} (R : Semiring a ℓ)
   where
 
 open Semiring R renaming (Carrier to A)
-open SemiringDiv R
+open import Algebra.Properties.Semiring.Divisibility R
 
 ------------------------------------------------------------------------------
 -- Re-export primality definitions
 
-open Algebra.Primality _≈_ _*_ 0# 1# public
-
-------------------------------------------------------------------------------
--- Properties of Irreducible
-
-Irreducible⇒≉0 : 0# ≉ 1# → ∀ {p} → Irreducible p → p ≉ 0#
-Irreducible⇒≉0 0≉1 (mkIrred _ chooseInvertible) p≈0 =
-  0∤1 0≉1 (reduce (chooseInvertible (trans p≈0 (sym (zeroˡ 0#)))))
+open import Algebra.Definitions.RawSemiring rawSemiring public
+  using (Coprime; Prime; mkPrime; Irreducible; mkIrred)
 
 ------------------------------------------------------------------------------
 -- Properties of Coprime
@@ -44,3 +32,10 @@ Coprime-sym coprime = flip coprime
 
 ∣1⇒Coprime : ∀ {x} y → x ∣ 1# → Coprime x y
 ∣1⇒Coprime {x} y x∣1 z∣x _ = ∣-trans z∣x x∣1
+
+------------------------------------------------------------------------------
+-- Properties of Irreducible
+
+Irreducible⇒≉0 : 0# ≉ 1# → ∀ {p} → Irreducible p → p ≉ 0#
+Irreducible⇒≉0 0≉1 (mkIrred _ chooseInvertible) p≈0 =
+  0∤1 0≉1 (reduce (chooseInvertible (trans p≈0 (sym (zeroˡ 0#)))))
diff --git a/src/Algebra/Solver/Ring/NaturalCoefficients.agda b/src/Algebra/Solver/Ring/NaturalCoefficients.agda
index 4aa0214089..9758c3db01 100644
--- a/src/Algebra/Solver/Ring/NaturalCoefficients.agda
+++ b/src/Algebra/Solver/Ring/NaturalCoefficients.agda
@@ -10,19 +10,19 @@
 open import Algebra
 import Algebra.Properties.Semiring.Multiplication as SemiringMultiplication
 open import Data.Maybe.Base using (Maybe; just; nothing; map)
+open import Algebra.Solver.Ring.AlmostCommutativeRing
+open import Data.Nat.Base as ℕ
+open import Data.Product using (module Σ)
+open import Function.Base using (id)
+open import Relation.Binary.PropositionalEquality using (_≡_)
 
 module Algebra.Solver.Ring.NaturalCoefficients
   {r₁ r₂} (R : CommutativeSemiring r₁ r₂)
   (open CommutativeSemiring R)
-  (open SemiringMultiplication semiring)
-  (dec : ∀ m n → Maybe (m × 1# ≈ n × 1#)) where
+  (open SemiringMultiplication semiring using () renaming (_×_ to _×ᵤ_))
+  (dec : ∀ m n → Maybe (m ×ᵤ 1# ≈ n ×ᵤ 1#)) where
 
-import Algebra.Solver.Ring
-open import Algebra.Solver.Ring.AlmostCommutativeRing
-open import Data.Nat.Base as ℕ
-open import Data.Product using (module Σ)
-open import Function
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Algebra.Properties.Semiring.Multiplication.TCOptimised semiring
 
 open import Relation.Binary.Reasoning.Setoid setoid
 
@@ -43,15 +43,15 @@ private
 
   -- There is a homomorphism from ℕ to R.
   --
-  -- Note that _×′_ is used rather than _×_. If _×_ were used, then
-  -- Function.Related.TypeIsomorphisms.test would fail to type-check.
+  -- Note that the optimised _×_ is used rather than unoptimised _×ᵤ_.
+  -- If _×ᵤ_ were used, then Function.Related.TypeIsomorphisms.test would fail
+  -- to type-check.
 
-  homomorphism :
-    ℕ-ring -Raw-AlmostCommutative⟶ fromCommutativeSemiring R
+  homomorphism : ℕ-ring -Raw-AlmostCommutative⟶ fromCommutativeSemiring R
   homomorphism = record
-    { ⟦_⟧    = λ n → n ×′ 1#
-    ; +-homo = ×′-homo-+ 1#
-    ; *-homo = ×′1-homo-*
+    { ⟦_⟧    = λ n → n × 1#
+    ; +-homo = ×-homo-+ 1#
+    ; *-homo = ×1-homo-*
     ; -‿homo = λ _ → refl
     ; 0-homo = refl
     ; 1-homo = refl
@@ -59,16 +59,16 @@ private
 
   -- Equality of certain expressions can be decided.
 
-  dec′ : ∀ m n → Maybe (m ×′ 1# ≈ n ×′ 1#)
+  dec′ : ∀ m n → Maybe (m × 1# ≈ n × 1#)
   dec′ m n = map to (dec m n)
     where
-    to : m × 1# ≈ n × 1# → m ×′ 1# ≈ n ×′ 1#
+    to : m ×ᵤ 1# ≈ n ×ᵤ 1# → m × 1# ≈ n × 1#
     to m≈n = begin
-      m ×′ 1#  ≈⟨ sym $ ×≈×′ m 1# ⟩
-      m ×  1#  ≈⟨ m≈n ⟩
-      n ×  1#  ≈⟨ ×≈×′ n 1# ⟩
-      n ×′ 1#  ∎
+      m ×  1#  ≈˘⟨ ×ᵤ≈× m 1# ⟩
+      m ×ᵤ 1#  ≈⟨  m≈n ⟩
+      n ×ᵤ 1#  ≈⟨  ×ᵤ≈× n 1# ⟩
+      n ×  1#  ∎
 
 -- The instantiation.
 
-open Algebra.Solver.Ring _ _ homomorphism dec′ public
+open import Algebra.Solver.Ring _ _ homomorphism dec′ public