Standardize scalar multiplication on all sorts of rings (#1707)

We had multiple competing definitions for rings, and many of the
definitions didn't use the perfectly applicable definition of multiples
for abelian groups...this is an attempt to standardize.

(I ran into this while working on #1700.)

Author: lowasser

src/commutative-algebra.lagda.md

@@ -42,6 +42,9 @@ open import commutative-algebra.large-commutative-rings public
 open import commutative-algebra.local-commutative-rings public
 open import commutative-algebra.maximal-ideals-commutative-rings public
 open import commutative-algebra.multiples-of-elements-commutative-rings public
+open import commutative-algebra.multiples-of-elements-commutative-semirings public
+open import commutative-algebra.multiples-of-elements-euclidean-domains public
+open import commutative-algebra.multiples-of-elements-integral-domains public
 open import commutative-algebra.nilradical-commutative-rings public
 open import commutative-algebra.nilradicals-commutative-semirings public
 open import commutative-algebra.polynomials-commutative-rings public

src/commutative-algebra/binomial-theorem-commutative-rings.lagda.md

@@ -9,6 +9,7 @@ module commutative-algebra.binomial-theorem-commutative-rings where
 ```agda
 open import commutative-algebra.binomial-theorem-commutative-semirings
 open import commutative-algebra.commutative-rings
+open import commutative-algebra.multiples-of-elements-commutative-rings
 open import commutative-algebra.powers-of-elements-commutative-rings
 open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-rings
 
@@ -168,7 +169,7 @@ is-linear-combination-power-add-Commutative-Ring :
       ( power-Commutative-Ring A m y)
       ( sum-fin-sequence-type-Commutative-Ring A n
         ( λ i →
-          mul-nat-scalar-Commutative-Ring A
+          multiple-Commutative-Ring A
             ( binomial-coefficient-ℕ (n +ℕ m) (nat-Fin n i))
             ( mul-Commutative-Ring A
               ( power-Commutative-Ring A (nat-Fin n i) x)
@@ -178,7 +179,7 @@ is-linear-combination-power-add-Commutative-Ring :
       ( sum-fin-sequence-type-Commutative-Ring A
         ( succ-ℕ m)
         ( λ i →
-          mul-nat-scalar-Commutative-Ring A
+          multiple-Commutative-Ring A
             ( binomial-coefficient-ℕ
               ( n +ℕ m)
               ( n +ℕ (nat-Fin (succ-ℕ m) i)))

src/commutative-algebra/binomial-theorem-commutative-semirings.lagda.md

@@ -8,6 +8,7 @@ module commutative-algebra.binomial-theorem-commutative-semirings where
 
 ```agda
 open import commutative-algebra.commutative-semirings
+open import commutative-algebra.multiples-of-elements-commutative-semirings
 open import commutative-algebra.powers-of-elements-commutative-semirings
 open import commutative-algebra.sums-of-finite-sequences-of-elements-commutative-semirings
 
@@ -167,7 +168,7 @@ is-linear-combination-power-add-Commutative-Semiring :
       ( power-Commutative-Semiring A m y)
       ( sum-fin-sequence-type-Commutative-Semiring A n
         ( λ i →
-          mul-nat-scalar-Commutative-Semiring A
+          multiple-Commutative-Semiring A
             ( binomial-coefficient-ℕ (n +ℕ m) (nat-Fin n i))
             ( mul-Commutative-Semiring A
               ( power-Commutative-Semiring A (nat-Fin n i) x)
@@ -177,7 +178,7 @@ is-linear-combination-power-add-Commutative-Semiring :
       ( sum-fin-sequence-type-Commutative-Semiring A
         ( succ-ℕ m)
         ( λ i →
-          mul-nat-scalar-Commutative-Semiring A
+          multiple-Commutative-Semiring A
             ( binomial-coefficient-ℕ
               ( n +ℕ m)
               ( n +ℕ (nat-Fin (succ-ℕ m) i)))

src/commutative-algebra/commutative-rings.lagda.md

@@ -583,74 +583,6 @@ module _
     right-distributive-mul-right-subtraction-Ring ring-Commutative-Ring
 ```
 
-### Scalar multiplication of elements of a commutative ring by natural numbers
-
-```agda
-  mul-nat-scalar-Commutative-Ring :
-    ℕ → type-Commutative-Ring → type-Commutative-Ring
-  mul-nat-scalar-Commutative-Ring =
-    mul-nat-scalar-Ring ring-Commutative-Ring
-
-  ap-mul-nat-scalar-Commutative-Ring :
-    {m n : ℕ} {x y : type-Commutative-Ring} →
-    (m ＝ n) → (x ＝ y) →
-    mul-nat-scalar-Commutative-Ring m x ＝
-    mul-nat-scalar-Commutative-Ring n y
-  ap-mul-nat-scalar-Commutative-Ring =
-    ap-mul-nat-scalar-Ring ring-Commutative-Ring
-
-  left-zero-law-mul-nat-scalar-Commutative-Ring :
-    (x : type-Commutative-Ring) →
-    mul-nat-scalar-Commutative-Ring 0 x ＝ zero-Commutative-Ring
-  left-zero-law-mul-nat-scalar-Commutative-Ring =
-    left-zero-law-mul-nat-scalar-Ring ring-Commutative-Ring
-
-  right-zero-law-mul-nat-scalar-Commutative-Ring :
-    (n : ℕ) →
-    mul-nat-scalar-Commutative-Ring n zero-Commutative-Ring ＝
-    zero-Commutative-Ring
-  right-zero-law-mul-nat-scalar-Commutative-Ring =
-    right-zero-law-mul-nat-scalar-Ring ring-Commutative-Ring
-
-  left-unit-law-mul-nat-scalar-Commutative-Ring :
-    (x : type-Commutative-Ring) →
-    mul-nat-scalar-Commutative-Ring 1 x ＝ x
-  left-unit-law-mul-nat-scalar-Commutative-Ring =
-    left-unit-law-mul-nat-scalar-Ring ring-Commutative-Ring
-
-  left-nat-scalar-law-mul-Commutative-Ring :
-    (n : ℕ) (x y : type-Commutative-Ring) →
-    mul-Commutative-Ring (mul-nat-scalar-Commutative-Ring n x) y ＝
-    mul-nat-scalar-Commutative-Ring n (mul-Commutative-Ring x y)
-  left-nat-scalar-law-mul-Commutative-Ring =
-    left-nat-scalar-law-mul-Ring ring-Commutative-Ring
-
-  right-nat-scalar-law-mul-Commutative-Ring :
-    (n : ℕ) (x y : type-Commutative-Ring) →
-    mul-Commutative-Ring x (mul-nat-scalar-Commutative-Ring n y) ＝
-    mul-nat-scalar-Commutative-Ring n (mul-Commutative-Ring x y)
-  right-nat-scalar-law-mul-Commutative-Ring =
-    right-nat-scalar-law-mul-Ring ring-Commutative-Ring
-
-  left-distributive-mul-nat-scalar-add-Commutative-Ring :
-    (n : ℕ) (x y : type-Commutative-Ring) →
-    mul-nat-scalar-Commutative-Ring n (add-Commutative-Ring x y) ＝
-    add-Commutative-Ring
-      ( mul-nat-scalar-Commutative-Ring n x)
-      ( mul-nat-scalar-Commutative-Ring n y)
-  left-distributive-mul-nat-scalar-add-Commutative-Ring =
-    left-distributive-mul-nat-scalar-add-Ring ring-Commutative-Ring
-
-  right-distributive-mul-nat-scalar-add-Commutative-Ring :
-    (m n : ℕ) (x : type-Commutative-Ring) →
-    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)
-  right-distributive-mul-nat-scalar-add-Commutative-Ring =
-    right-distributive-mul-nat-scalar-add-Ring ring-Commutative-Ring
-```
-
 ### Addition of a list of elements in a commutative ring
 
 ```agda

src/commutative-algebra/commutative-semirings.lagda.md

@@ -283,73 +283,3 @@ module _
       ( commutative-mul-Commutative-Semiring)
       ( associative-mul-Commutative-Semiring)
 ```
-
-## Operations
-
-### Scalar multiplication of elements of a commutative ring by natural numbers
-
-```agda
-  mul-nat-scalar-Commutative-Semiring :
-    ℕ → type-Commutative-Semiring → type-Commutative-Semiring
-  mul-nat-scalar-Commutative-Semiring =
-    mul-nat-scalar-Semiring semiring-Commutative-Semiring
-
-  ap-mul-nat-scalar-Commutative-Semiring :
-    {m n : ℕ} {x y : type-Commutative-Semiring} →
-    (m ＝ n) → (x ＝ y) →
-    mul-nat-scalar-Commutative-Semiring m x ＝
-    mul-nat-scalar-Commutative-Semiring n y
-  ap-mul-nat-scalar-Commutative-Semiring =
-    ap-mul-nat-scalar-Semiring semiring-Commutative-Semiring
-
-  left-zero-law-mul-nat-scalar-Commutative-Semiring :
-    (x : type-Commutative-Semiring) →
-    mul-nat-scalar-Commutative-Semiring 0 x ＝ zero-Commutative-Semiring
-  left-zero-law-mul-nat-scalar-Commutative-Semiring =
-    left-zero-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring
-
-  right-zero-law-mul-nat-scalar-Commutative-Semiring :
-    (n : ℕ) →
-    mul-nat-scalar-Commutative-Semiring n zero-Commutative-Semiring ＝
-    zero-Commutative-Semiring
-  right-zero-law-mul-nat-scalar-Commutative-Semiring =
-    right-zero-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring
-
-  left-unit-law-mul-nat-scalar-Commutative-Semiring :
-    (x : type-Commutative-Semiring) →
-    mul-nat-scalar-Commutative-Semiring 1 x ＝ x
-  left-unit-law-mul-nat-scalar-Commutative-Semiring =
-    left-unit-law-mul-nat-scalar-Semiring semiring-Commutative-Semiring
-
-  left-nat-scalar-law-mul-Commutative-Semiring :
-    (n : ℕ) (x y : type-Commutative-Semiring) →
-    mul-Commutative-Semiring (mul-nat-scalar-Commutative-Semiring n x) y ＝
-    mul-nat-scalar-Commutative-Semiring n (mul-Commutative-Semiring x y)
-  left-nat-scalar-law-mul-Commutative-Semiring =
-    left-nat-scalar-law-mul-Semiring semiring-Commutative-Semiring
-
-  right-nat-scalar-law-mul-Commutative-Semiring :
-    (n : ℕ) (x y : type-Commutative-Semiring) →
-    mul-Commutative-Semiring x (mul-nat-scalar-Commutative-Semiring n y) ＝
-    mul-nat-scalar-Commutative-Semiring n (mul-Commutative-Semiring x y)
-  right-nat-scalar-law-mul-Commutative-Semiring =
-    right-nat-scalar-law-mul-Semiring semiring-Commutative-Semiring
-
-  left-distributive-mul-nat-scalar-add-Commutative-Semiring :
-    (n : ℕ) (x y : type-Commutative-Semiring) →
-    mul-nat-scalar-Commutative-Semiring n (add-Commutative-Semiring x y) ＝
-    add-Commutative-Semiring
-      ( mul-nat-scalar-Commutative-Semiring n x)
-      ( mul-nat-scalar-Commutative-Semiring n y)
-  left-distributive-mul-nat-scalar-add-Commutative-Semiring =
-    left-distributive-mul-nat-scalar-add-Semiring semiring-Commutative-Semiring
-
-  right-distributive-mul-nat-scalar-add-Commutative-Semiring :
-    (m n : ℕ) (x : type-Commutative-Semiring) →
-    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)
-  right-distributive-mul-nat-scalar-add-Commutative-Semiring =
-    right-distributive-mul-nat-scalar-add-Semiring semiring-Commutative-Semiring
-```

src/commutative-algebra/euclidean-domains.lagda.md

@@ -52,8 +52,9 @@ open import ring-theory.semirings
 
 ## Idea
 
-A **Euclidean domain** is an
-[integral domain](commutative-algebra.integral-domains.md) `R` that has a
+A
+{{#concept "Euclidean domain" Agda=Euclidean-Domain WDID=Q867345 WD="Euclidean domain"}}
+is an [integral domain](commutative-algebra.integral-domains.md) `R` that has a
 **Euclidean valuation**, i.e., a function `v : R → ℕ` such that for every
 `x y : R`, if `y` is nonzero then there are `q r : R` with `x = q y + r` and
 `v r < v y`.
@@ -544,83 +545,6 @@ module _
       integral-domain-Euclidean-Domain
 ```
 
-### Scalar multiplication of elements of a Euclidean domain by natural numbers
-
-```agda
-  mul-nat-scalar-Euclidean-Domain :
-    ℕ → type-Euclidean-Domain → type-Euclidean-Domain
-  mul-nat-scalar-Euclidean-Domain =
-    mul-nat-scalar-Integral-Domain
-      integral-domain-Euclidean-Domain
-
-  ap-mul-nat-scalar-Euclidean-Domain :
-    {m n : ℕ} {x y : type-Euclidean-Domain} →
-    (m ＝ n) → (x ＝ y) →
-    mul-nat-scalar-Euclidean-Domain m x ＝
-    mul-nat-scalar-Euclidean-Domain n y
-  ap-mul-nat-scalar-Euclidean-Domain =
-    ap-mul-nat-scalar-Integral-Domain
-      integral-domain-Euclidean-Domain
-
-  left-zero-law-mul-nat-scalar-Euclidean-Domain :
-    (x : type-Euclidean-Domain) →
-    mul-nat-scalar-Euclidean-Domain 0 x ＝ zero-Euclidean-Domain
-  left-zero-law-mul-nat-scalar-Euclidean-Domain =
-    left-zero-law-mul-nat-scalar-Integral-Domain
-      integral-domain-Euclidean-Domain
-
-  right-zero-law-mul-nat-scalar-Euclidean-Domain :
-    (n : ℕ) →
-    mul-nat-scalar-Euclidean-Domain n zero-Euclidean-Domain ＝
-    zero-Euclidean-Domain
-  right-zero-law-mul-nat-scalar-Euclidean-Domain =
-    right-zero-law-mul-nat-scalar-Integral-Domain
-      integral-domain-Euclidean-Domain
-
-  left-unit-law-mul-nat-scalar-Euclidean-Domain :
-    (x : type-Euclidean-Domain) →
-    mul-nat-scalar-Euclidean-Domain 1 x ＝ x
-  left-unit-law-mul-nat-scalar-Euclidean-Domain =
-    left-unit-law-mul-nat-scalar-Integral-Domain
-      integral-domain-Euclidean-Domain
-
-  left-nat-scalar-law-mul-Euclidean-Domain :
-    (n : ℕ) (x y : type-Euclidean-Domain) →
-    mul-Euclidean-Domain (mul-nat-scalar-Euclidean-Domain n x) y ＝
-    mul-nat-scalar-Euclidean-Domain n (mul-Euclidean-Domain x y)
-  left-nat-scalar-law-mul-Euclidean-Domain =
-    left-nat-scalar-law-mul-Integral-Domain
-      integral-domain-Euclidean-Domain
-
-  right-nat-scalar-law-mul-Euclidean-Domain :
-    (n : ℕ) (x y : type-Euclidean-Domain) →
-    mul-Euclidean-Domain x (mul-nat-scalar-Euclidean-Domain n y) ＝
-    mul-nat-scalar-Euclidean-Domain n (mul-Euclidean-Domain x y)
-  right-nat-scalar-law-mul-Euclidean-Domain =
-    right-nat-scalar-law-mul-Integral-Domain
-      integral-domain-Euclidean-Domain
-
-  left-distributive-mul-nat-scalar-add-Euclidean-Domain :
-    (n : ℕ) (x y : type-Euclidean-Domain) →
-    mul-nat-scalar-Euclidean-Domain n (add-Euclidean-Domain x y) ＝
-    add-Euclidean-Domain
-      ( mul-nat-scalar-Euclidean-Domain n x)
-      ( mul-nat-scalar-Euclidean-Domain n y)
-  left-distributive-mul-nat-scalar-add-Euclidean-Domain =
-    left-distributive-mul-nat-scalar-add-Integral-Domain
-      integral-domain-Euclidean-Domain
-
-  right-distributive-mul-nat-scalar-add-Euclidean-Domain :
-    (m n : ℕ) (x : type-Euclidean-Domain) →
-    mul-nat-scalar-Euclidean-Domain (m +ℕ n) x ＝
-    add-Euclidean-Domain
-      ( mul-nat-scalar-Euclidean-Domain m x)
-      ( mul-nat-scalar-Euclidean-Domain n x)
-  right-distributive-mul-nat-scalar-add-Euclidean-Domain =
-    right-distributive-mul-nat-scalar-add-Integral-Domain
-      integral-domain-Euclidean-Domain
-```
-
 ### Addition of a list of elements in a Euclidean domain
 
 ```agda

src/commutative-algebra/integer-multiples-of-elements-commutative-rings.lagda.md

@@ -119,10 +119,10 @@ module _
   {l : Level} (A : Commutative-Ring l) (a : type-Commutative-Ring A)
   where
 
-  integer-multiple-zero-Commutative-Ring :
+  integer-right-zero-law-multiple-Commutative-Ring :
     integer-multiple-Commutative-Ring A zero-ℤ a ＝ zero-Commutative-Ring A
-  integer-multiple-zero-Commutative-Ring =
-    integer-multiple-zero-Ring (ring-Commutative-Ring A) a
+  integer-right-zero-law-multiple-Commutative-Ring =
+    left-zero-law-integer-multiple-Ring (ring-Commutative-Ring A) a
 ```
 
 ### `1x ＝ x`