Refactor to use infix binary operators for arithmetic (UniMath#620)

- Refactor to use infix binary operators for arithmetic. - Define infix binary operators for arithmetic operations on the Eisenstein integers, Gaussian integers,half integers, and truncation levels. - Swap to using left/right instead of a `'` for different laws for binary arithmetic operators. - Some additional refactoring for Eisenstein integers and Gaussian integers Note that the non-infix variants of the operators are still used some places, matching how `Id` and `pair` are used.
fredrik-bakke · May 18, 2023 · 001e8d7 · 001e8d7
1 parent fde878d
commit 001e8d7
Show file tree

Hide file tree

Showing 121 changed files with 1,872 additions and 2,012 deletions.
diff --git a/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md
@@ -145,14 +145,14 @@ binomial-theorem-Commutative-Ring A n x y =
 is-linear-combination-power-add-Commutative-Ring :
   {l : Level} (A : Commutative-Ring l) (n m : ℕ)
   (x y : type-Commutative-Ring A) →
-  power-Commutative-Ring A (add-ℕ n m) (add-Commutative-Ring A x y) ＝
+  power-Commutative-Ring A (n +ℕ m) (add-Commutative-Ring A x y) ＝
   add-Commutative-Ring A
     ( mul-Commutative-Ring A
       ( power-Commutative-Ring A m y)
       ( sum-Commutative-Ring A n
         ( λ i →
           mul-nat-scalar-Commutative-Ring A
-            ( binomial-coefficient-ℕ (add-ℕ n m) (nat-Fin n i))
+            ( binomial-coefficient-ℕ (n +ℕ m) (nat-Fin n i))
             ( mul-Commutative-Ring A
               ( power-Commutative-Ring A (nat-Fin n i) x)
               ( power-Commutative-Ring A (dist-ℕ (nat-Fin n i) n) y)))))
@@ -163,8 +163,8 @@ is-linear-combination-power-add-Commutative-Ring :
         ( λ i →
           mul-nat-scalar-Commutative-Ring A
             ( binomial-coefficient-ℕ
-              ( add-ℕ n m)
-              ( add-ℕ n (nat-Fin (succ-ℕ m) i)))
+              ( n +ℕ m)
+              ( n +ℕ (nat-Fin (succ-ℕ m) i)))
             ( mul-Commutative-Ring A
               ( power-Commutative-Ring A (nat-Fin (succ-ℕ m) i) x)
               ( power-Commutative-Ring A

diff --git a/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md b/src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md
@@ -151,14 +151,14 @@ binomial-theorem-Commutative-Semiring A n x y =
 is-linear-combination-power-add-Commutative-Semiring :
   {l : Level} (A : Commutative-Semiring l) (n m : ℕ)
   (x y : type-Commutative-Semiring A) →
-  power-Commutative-Semiring A (add-ℕ n m) (add-Commutative-Semiring A x y) ＝
+  power-Commutative-Semiring A (n +ℕ m) (add-Commutative-Semiring A x y) ＝
   add-Commutative-Semiring A
     ( mul-Commutative-Semiring A
       ( power-Commutative-Semiring A m y)
       ( sum-Commutative-Semiring A n
         ( λ i →
           mul-nat-scalar-Commutative-Semiring A
-            ( binomial-coefficient-ℕ (add-ℕ n m) (nat-Fin n i))
+            ( binomial-coefficient-ℕ (n +ℕ m) (nat-Fin n i))
             ( mul-Commutative-Semiring A
               ( power-Commutative-Semiring A (nat-Fin n i) x)
               ( power-Commutative-Semiring A (dist-ℕ (nat-Fin n i) n) y)))))
@@ -169,8 +169,8 @@ is-linear-combination-power-add-Commutative-Semiring :
         ( λ i →
           mul-nat-scalar-Commutative-Semiring A
             ( binomial-coefficient-ℕ
-              ( add-ℕ n m)
-              ( add-ℕ n (nat-Fin (succ-ℕ m) i)))
+              ( n +ℕ m)
+              ( n +ℕ (nat-Fin (succ-ℕ m) i)))
             ( mul-Commutative-Semiring A
               ( power-Commutative-Semiring A (nat-Fin (succ-ℕ m) i) x)
               ( power-Commutative-Semiring A

diff --git a/src/commutative-algebra/commutative-rings.lagda.md b/src/commutative-algebra/commutative-rings.lagda.md
@@ -525,7 +525,7 @@ module _
 
   right-distributive-mul-nat-scalar-add-Commutative-Ring :
     (m n : ℕ) (x : type-Commutative-Ring) →
-    mul-nat-scalar-Commutative-Ring (add-ℕ m n) x ＝
+    mul-nat-scalar-Commutative-Ring (m +ℕ n) x ＝
     add-Commutative-Ring
       ( mul-nat-scalar-Commutative-Ring m x)
       ( mul-nat-scalar-Commutative-Ring n x)

diff --git a/src/commutative-algebra/commutative-semirings.lagda.md b/src/commutative-algebra/commutative-semirings.lagda.md
@@ -309,7 +309,7 @@ module _
 
   right-distributive-mul-nat-scalar-add-Commutative-Semiring :
     (m n : ℕ) (x : type-Commutative-Semiring) →
-    mul-nat-scalar-Commutative-Semiring (add-ℕ m n) x ＝
+    mul-nat-scalar-Commutative-Semiring (m +ℕ n) x ＝
     add-Commutative-Semiring
       ( mul-nat-scalar-Commutative-Semiring m x)
       ( mul-nat-scalar-Commutative-Semiring n x)