Define binary operator notations for mul-ℕ, mul-ℤ, and exp-ℕ. (#…

…618)

They are `_*ℕ_`, `_*ℤ_`, and `_^ℕ_` respectively.

In addition to what the title says, I've also refactored the files
- `multiplication-natural-numbers`
- `multiplication-integers`
- `exponentiation-natural-numbers`
- `absolute-value-integers`

to use the binary operators where it's natural, to get a sense for how
this would look. It should be possible to change most usages easily
enough* with a nice enough regex, but I don't want to do this before I
get some feedback on whether it is preferable.

Also, pairs like `is-injective-mul-succ-ℕ` and
`is-injective-mul-succ-ℕ'` should perhaps be renamed to something like
`is-injective-left-mul-succ-ℕ` and `is-injective-right-mul-succ-ℕ`.

src/elementary-number-theory/absolute-value-integers.lagda.md

@@ -111,7 +111,7 @@ successor-law-abs-ℤ (inr (inr x)) =
 
 ```agda
 subadditive-abs-ℤ :
-  (x y : ℤ) → (abs-ℤ (add-ℤ x y)) ≤-ℕ (add-ℕ (abs-ℤ x) (abs-ℤ y))
+  (x y : ℤ) → (abs-ℤ (x +ℤ y)) ≤-ℕ ((abs-ℤ x) +ℕ (abs-ℤ y))
 subadditive-abs-ℤ x (inl zero-ℕ) =
   concatenate-eq-leq-eq-ℕ
     ( ap abs-ℤ (add-neg-one-right-ℤ x))
@@ -121,11 +121,11 @@ subadditive-abs-ℤ x (inl (succ-ℕ y)) =
   concatenate-eq-leq-eq-ℕ
     ( ap abs-ℤ (right-predecessor-law-add-ℤ x (inl y)))
     ( transitive-leq-ℕ
-      ( abs-ℤ (pred-ℤ (add-ℤ x (inl y))))
-      ( succ-ℕ (abs-ℤ (add-ℤ x (inl y))))
-      ( add-ℕ (abs-ℤ x) (succ-ℕ (succ-ℕ y)))
+      ( abs-ℤ (pred-ℤ (x +ℤ (inl y))))
+      ( succ-ℕ (abs-ℤ (x +ℤ (inl y))))
+      ( (abs-ℤ x) +ℕ (succ-ℕ (succ-ℕ y)))
       ( subadditive-abs-ℤ x (inl y))
-      ( predecessor-law-abs-ℤ (add-ℤ x (inl y))))
+      ( predecessor-law-abs-ℤ (x +ℤ (inl y))))
     ( refl)
 subadditive-abs-ℤ x (inr (inl star)) =
   concatenate-eq-leq-eq-ℕ
@@ -141,11 +141,11 @@ subadditive-abs-ℤ x (inr (inr (succ-ℕ y))) =
   concatenate-eq-leq-eq-ℕ
     ( ap abs-ℤ (right-successor-law-add-ℤ x (inr (inr y))))
     ( transitive-leq-ℕ
-      ( abs-ℤ (succ-ℤ (add-ℤ x (inr (inr y)))))
-      ( succ-ℕ (abs-ℤ (add-ℤ x (inr (inr y)))))
-      ( succ-ℕ (add-ℕ (abs-ℤ x) (succ-ℕ y)))
+      ( abs-ℤ (succ-ℤ (x +ℤ (inr (inr y)))))
+      ( succ-ℕ (abs-ℤ (x +ℤ (inr (inr y)))))
+      ( succ-ℕ ((abs-ℤ x) +ℕ (succ-ℕ y)))
       ( subadditive-abs-ℤ x (inr (inr y)))
-      ( successor-law-abs-ℤ (add-ℤ x (inr (inr y)))))
+      ( successor-law-abs-ℤ (x +ℤ (inr (inr y)))))
     ( refl)
 ```
 
@@ -179,19 +179,19 @@ is-nonzero-abs-ℤ (inr (inr x)) H = is-nonzero-succ-ℕ x
 
 ```agda
 multiplicative-abs-ℤ' :
-  (x y : ℤ) → abs-ℤ (explicit-mul-ℤ x y) ＝ mul-ℕ (abs-ℤ x) (abs-ℤ y)
+  (x y : ℤ) → abs-ℤ (explicit-mul-ℤ x y) ＝ (abs-ℤ x) *ℕ (abs-ℤ y)
 multiplicative-abs-ℤ' (inl x) (inl y) =
   abs-int-ℕ _
 multiplicative-abs-ℤ' (inl x) (inr (inl star)) =
   inv (right-zero-law-mul-ℕ x)
 multiplicative-abs-ℤ' (inl x) (inr (inr y)) =
-  ( abs-neg-ℤ (inl (add-ℕ (mul-ℕ x (succ-ℕ y)) y))) ∙
-  ( abs-int-ℕ (mul-ℕ (succ-ℕ x) (succ-ℕ y)))
+  ( abs-neg-ℤ (inl ((x *ℕ (succ-ℕ y)) +ℕ y))) ∙
+  ( abs-int-ℕ ((succ-ℕ x) *ℕ (succ-ℕ y)))
 multiplicative-abs-ℤ' (inr (inl star)) (inl y) =
   refl
 multiplicative-abs-ℤ' (inr (inr x)) (inl y) =
-  ( abs-neg-ℤ (inl (add-ℕ (mul-ℕ x (succ-ℕ y)) y))) ∙
-  ( abs-int-ℕ (succ-ℕ (add-ℕ (mul-ℕ x (succ-ℕ y)) y)))
+  ( abs-neg-ℤ (inl ((x *ℕ (succ-ℕ y)) +ℕ y))) ∙
+  ( abs-int-ℕ (succ-ℕ ((x *ℕ (succ-ℕ y)) +ℕ y)))
 multiplicative-abs-ℤ' (inr (inl star)) (inr (inl star)) =
   refl
 multiplicative-abs-ℤ' (inr (inl star)) (inr (inr x)) =
@@ -202,7 +202,7 @@ multiplicative-abs-ℤ' (inr (inr x)) (inr (inr y)) =
   abs-int-ℕ _
 
 multiplicative-abs-ℤ :
-  (x y : ℤ) → abs-ℤ (mul-ℤ x y) ＝ mul-ℕ (abs-ℤ x) (abs-ℤ y)
+  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ (abs-ℤ x) *ℕ (abs-ℤ y)
 multiplicative-abs-ℤ x y =
   ap abs-ℤ (compute-mul-ℤ x y) ∙ multiplicative-abs-ℤ' x y
 ```
@@ -211,35 +211,35 @@ multiplicative-abs-ℤ x y =
 
 ```agda
 left-negative-law-mul-abs-ℤ :
-  (x y : ℤ) → abs-ℤ (mul-ℤ x y) ＝ abs-ℤ (mul-ℤ (neg-ℤ x) y)
+  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ ((neg-ℤ x) *ℤ y)
 left-negative-law-mul-abs-ℤ x y =
   equational-reasoning
-    abs-ℤ (mul-ℤ x y)
-    ＝ abs-ℤ (neg-ℤ (mul-ℤ x y))
-      by (inv (negative-law-abs-ℤ (mul-ℤ x y)))
-    ＝ abs-ℤ (mul-ℤ (neg-ℤ x) y)
+    abs-ℤ (x *ℤ y)
+    ＝ abs-ℤ (neg-ℤ (x *ℤ y))
+      by (inv (negative-law-abs-ℤ (x *ℤ y)))
+    ＝ abs-ℤ ((neg-ℤ x) *ℤ y)
       by (ap abs-ℤ (inv (left-negative-law-mul-ℤ x y)))
 ```
 
 ### `|x(-y)| ＝ |xy|`
 
 ```agda
 right-negative-law-mul-abs-ℤ :
-  (x y : ℤ) → abs-ℤ (mul-ℤ x y) ＝ abs-ℤ (mul-ℤ x (neg-ℤ y))
+  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ (x *ℤ (neg-ℤ y))
 right-negative-law-mul-abs-ℤ x y =
   equational-reasoning
-    abs-ℤ (mul-ℤ x y)
-    ＝ abs-ℤ (neg-ℤ (mul-ℤ x y))
-      by (inv (negative-law-abs-ℤ (mul-ℤ x y)))
-    ＝ abs-ℤ (mul-ℤ x (neg-ℤ y))
+    abs-ℤ (x *ℤ y)
+    ＝ abs-ℤ (neg-ℤ (x *ℤ y))
+      by (inv (negative-law-abs-ℤ (x *ℤ y)))
+    ＝ abs-ℤ (x *ℤ (neg-ℤ y))
       by (ap abs-ℤ (inv (right-negative-law-mul-ℤ x y)))
 ```
 
 ### `|(-x)(-y)| ＝ |xy|`
 
 ```agda
 double-negative-law-mul-abs-ℤ :
-  (x y : ℤ) → abs-ℤ (mul-ℤ x y) ＝ abs-ℤ (mul-ℤ (neg-ℤ x) (neg-ℤ y))
+  (x y : ℤ) → abs-ℤ (x *ℤ y) ＝ abs-ℤ ((neg-ℤ x) *ℤ (neg-ℤ y))
 double-negative-law-mul-abs-ℤ x y =
   (right-negative-law-mul-abs-ℤ x y) ∙ (left-negative-law-mul-abs-ℤ x (neg-ℤ y))
 ```

src/elementary-number-theory/exponentiation-natural-numbers.lagda.md

@@ -27,9 +27,12 @@ times.
 ## Definition
 
 ```agda
-exp-ℕ : ℕ → (ℕ → ℕ)
+exp-ℕ : ℕ → ℕ → ℕ
 exp-ℕ m 0 = 1
 exp-ℕ m (succ-ℕ n) = mul-ℕ (exp-ℕ m n) m
+
+infix 30 _^ℕ_
+_^ℕ_ = exp-ℕ
 ```
 
 ```agda
@@ -42,39 +45,39 @@ power-ℕ = power-Commutative-Semiring ℕ-Commutative-Semiring
 ### Tarski's high school arithmetic laws for exponentiation
 
 ```agda
-annihilation-law-exp-ℕ : (n : ℕ) → exp-ℕ 1 n ＝ 1
+annihilation-law-exp-ℕ : (n : ℕ) → 1 ^ℕ n ＝ 1
 annihilation-law-exp-ℕ zero-ℕ = refl
 annihilation-law-exp-ℕ (succ-ℕ n) =
-  right-unit-law-mul-ℕ (exp-ℕ 1 n) ∙ annihilation-law-exp-ℕ n
+  right-unit-law-mul-ℕ (1 ^ℕ n) ∙ annihilation-law-exp-ℕ n
 
 left-distributive-exp-add-ℕ :
-  (x y z : ℕ) → exp-ℕ x (add-ℕ y z) ＝ mul-ℕ (exp-ℕ x y) (exp-ℕ x z)
-left-distributive-exp-add-ℕ x y zero-ℕ = inv (right-unit-law-mul-ℕ (exp-ℕ x y))
+  (x y z : ℕ) → x ^ℕ (y +ℕ z) ＝ (x ^ℕ y) *ℕ (x ^ℕ z)
+left-distributive-exp-add-ℕ x y zero-ℕ = inv (right-unit-law-mul-ℕ (x ^ℕ y))
 left-distributive-exp-add-ℕ x y (succ-ℕ z) =
-  ( ap (mul-ℕ' x) (left-distributive-exp-add-ℕ x y z)) ∙
-  ( associative-mul-ℕ (exp-ℕ x y) (exp-ℕ x z) x)
+  ( ap (_*ℕ x) (left-distributive-exp-add-ℕ x y z)) ∙
+  ( associative-mul-ℕ (x ^ℕ y) (x ^ℕ z) x)
 
 right-distributive-exp-mul-ℕ :
-  (x y z : ℕ) → exp-ℕ (mul-ℕ x y) z ＝ mul-ℕ (exp-ℕ x z) (exp-ℕ y z)
+  (x y z : ℕ) → (x *ℕ y) ^ℕ z ＝ (x ^ℕ z) *ℕ (y ^ℕ z)
 right-distributive-exp-mul-ℕ x y zero-ℕ = refl
 right-distributive-exp-mul-ℕ x y (succ-ℕ z) =
-  ( ap (mul-ℕ' (mul-ℕ x y)) (right-distributive-exp-mul-ℕ x y z)) ∙
-  ( interchange-law-mul-mul-ℕ (exp-ℕ x z) (exp-ℕ y z) x y)
+  ( ap (_*ℕ (x *ℕ y)) (right-distributive-exp-mul-ℕ x y z)) ∙
+  ( interchange-law-mul-mul-ℕ (x ^ℕ z) (y ^ℕ z) x y)
 
-exp-mul-ℕ : (x y z : ℕ) → exp-ℕ x (mul-ℕ y z) ＝ exp-ℕ (exp-ℕ x y) z
+exp-mul-ℕ : (x y z : ℕ) → x ^ℕ (y *ℕ z) ＝ (x ^ℕ y) ^ℕ z
 exp-mul-ℕ x zero-ℕ z = inv (annihilation-law-exp-ℕ z)
 exp-mul-ℕ x (succ-ℕ y) z =
-  ( left-distributive-exp-add-ℕ x (mul-ℕ y z) z) ∙
-  ( ( ap (mul-ℕ' (exp-ℕ x z)) (exp-mul-ℕ x y z)) ∙
-    ( inv (right-distributive-exp-mul-ℕ (exp-ℕ x y) x z)))
+  ( left-distributive-exp-add-ℕ x (y *ℕ z) z) ∙
+  ( ( ap (_*ℕ (x ^ℕ z)) (exp-mul-ℕ x y z)) ∙
+    ( inv (right-distributive-exp-mul-ℕ (x ^ℕ y) x z)))
 ```
 
 ### The exponent `m^n` is always nonzero
 
 ```agda
 is-nonzero-exp-ℕ :
-  (m n : ℕ) → is-nonzero-ℕ m → is-nonzero-ℕ (exp-ℕ m n)
+  (m n : ℕ) → is-nonzero-ℕ m → is-nonzero-ℕ (m ^ℕ n)
 is-nonzero-exp-ℕ m zero-ℕ p = is-nonzero-one-ℕ
 is-nonzero-exp-ℕ m (succ-ℕ n) p =
-  is-nonzero-mul-ℕ (exp-ℕ m n) m (is-nonzero-exp-ℕ m n p) p
+  is-nonzero-mul-ℕ (m ^ℕ n) m (is-nonzero-exp-ℕ m n p) p
 ```