tables

src/elementary-number-theory.lagda.md

@@ -53,7 +53,6 @@ open import elementary-number-theory.goldbach-conjecture public
 open import elementary-number-theory.greatest-common-divisor-integers public
 open import elementary-number-theory.greatest-common-divisor-natural-numbers public
 open import elementary-number-theory.group-of-integers public
-open import elementary-number-theory.groups-of-modular-arithmetic public
 open import elementary-number-theory.half-integers public
 open import elementary-number-theory.inequality-integer-fractions public
 open import elementary-number-theory.inequality-integers public
@@ -85,7 +84,7 @@ open import elementary-number-theory.multiplication-natural-numbers public
 open import elementary-number-theory.multiplication-rational-numbers public
 open import elementary-number-theory.multiplicative-monoid-of-natural-numbers public
 open import elementary-number-theory.multiplicative-units-integers public
-open import elementary-number-theory.multiplicative-units-modular-arithmetic public
+open import elementary-number-theory.multiplicative-units-standard-cyclic-rings public
 open import elementary-number-theory.multiset-coefficients public
 open import elementary-number-theory.natural-numbers public
 open import elementary-number-theory.nonzero-integers public
@@ -107,12 +106,13 @@ open import elementary-number-theory.relatively-prime-natural-numbers public
 open import elementary-number-theory.repeating-element-standard-finite-type public
 open import elementary-number-theory.retracts-of-natural-numbers public
 open import elementary-number-theory.ring-of-integers public
-open import elementary-number-theory.rings-of-modular-arithmetic public
 open import elementary-number-theory.sieve-of-eratosthenes public
 open import elementary-number-theory.square-free-natural-numbers public
 open import elementary-number-theory.squares-integers public
 open import elementary-number-theory.squares-modular-arithmetic public
 open import elementary-number-theory.squares-natural-numbers public
+open import elementary-number-theory.standard-cyclic-groups public
+open import elementary-number-theory.standard-cyclic-rings public
 open import elementary-number-theory.stirling-numbers-of-the-second-kind public
 open import elementary-number-theory.strict-inequality-natural-numbers public
 open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public

src/elementary-number-theory/eulers-totient-function.lagda.md

@@ -29,7 +29,7 @@ open import univalent-combinatorics.standard-finite-types
 **Euler's totient function** `φ : ℕ → ℕ` is the function that maps a
 [natural number](elementary-number-theory.natural-numbers.md) `n` to the number
 of
-[multiplicative units modulo `n`](elementary-number-theory.multiplicative-units-modular-arithmetic.md).
+[multiplicative units modulo `n`](elementary-number-theory.multiplicative-units-standard-cyclic-rings.md).
 In other words, the number `φ n` is the cardinality of the
 [group of units](ring-theory.groups-of-units-rings.md) of the
 [ring](ring-theory.rings.md) `ℤ-Mod n`.
@@ -58,3 +58,9 @@ eulers-totient-function-relatively-prime n =
     ( Fin-𝔽 n)
     ( λ x → is-relatively-prime-ℕ-Decidable-Prop (nat-Fin n x) n)
 ```
+
+## See also
+
+### Table of files related to cyclic types, groups, and rings
+
+{{#include tables/cyclic-types.md}}

src/elementary-number-theory/finitely-cyclic-maps.lagda.md

@@ -118,3 +118,9 @@ pr2 (is-finitely-cyclic-succ-Fin {succ-ℕ k} x y) =
           ( ( ap (add-Fin (succ-ℕ k) y) (left-inverse-law-add-Fin k x)) ∙
             ( right-unit-law-add-Fin k y)))))
 ```
+
+## See also
+
+### Table of files related to cyclic types, groups, and rings
+
+{{#include tables/cyclic-types.md}}

src/elementary-number-theory/multiplicative-units-standard-cyclic-rings.lagda.md

@@ -0,0 +1,19 @@
+# Multiplicative units in modular arithmetic
+
+```agda
+module elementary-number-theory.multiplicative-units-standard-cyclic-rings where
+```
+
+<details><summary>Imports</summary>
+
+```agda
+
+```
+
+</details>
+
+## See also
+
+### Table of files related to cyclic types, groups, and rings
+
+{{#include tables/cyclic-types.md}}

src/elementary-number-theory/relatively-prime-natural-numbers.lagda.md

@@ -17,7 +17,7 @@ open import elementary-number-theory.modular-arithmetic
 open import elementary-number-theory.multiplication-integers
 open import elementary-number-theory.natural-numbers
 open import elementary-number-theory.prime-numbers
-open import elementary-number-theory.rings-of-modular-arithmetic
+open import elementary-number-theory.standard-cyclic-rings
 
 open import foundation.decidable-propositions
 open import foundation.decidable-types

src/elementary-number-theory/ring-of-integers.lagda.md

@@ -159,3 +159,34 @@ is-initial-ℤ-Ring : is-initial-Ring ℤ-Ring
 pr1 (is-initial-ℤ-Ring S) = initial-hom-Ring S
 pr2 (is-initial-ℤ-Ring S) f = contraction-initial-hom-Ring S f
 ```
+
+### Integer multiplication in the ring of integers coincides with multiplication of integers
+
+```agda
+integer-multiple-one-ℤ-Ring :
+  (k : ℤ) → integer-multiple-Ring ℤ-Ring k one-ℤ ＝ k
+integer-multiple-one-ℤ-Ring (inl zero-ℕ) = refl
+integer-multiple-one-ℤ-Ring (inl (succ-ℕ n)) =
+  ap pred-ℤ (integer-multiple-one-ℤ-Ring (inl n))
+integer-multiple-one-ℤ-Ring (inr (inl star)) = refl
+integer-multiple-one-ℤ-Ring (inr (inr zero-ℕ)) = refl
+integer-multiple-one-ℤ-Ring (inr (inr (succ-ℕ n))) =
+  ap succ-ℤ (integer-multiple-one-ℤ-Ring (inr (inr n)))
+
+compute-integer-multiple-ℤ-Ring :
+  (k l : ℤ) → integer-multiple-Ring ℤ-Ring k l ＝ mul-ℤ k l
+compute-integer-multiple-ℤ-Ring k l =
+  equational-reasoning
+    integer-multiple-Ring ℤ-Ring k l
+    ＝ integer-multiple-Ring ℤ-Ring k (integer-multiple-Ring ℤ-Ring l one-ℤ)
+      by
+      ap
+        ( integer-multiple-Ring ℤ-Ring k)
+        ( inv (integer-multiple-one-ℤ-Ring l))
+    ＝ integer-multiple-Ring ℤ-Ring (mul-ℤ k l) one-ℤ
+      by
+      inv (integer-multiple-mul-Ring ℤ-Ring k l one-ℤ)
+    ＝ mul-ℤ k l
+      by
+      integer-multiple-one-ℤ-Ring _
+```

src/elementary-number-theory/groups-of-modular-arithmetic.lagda.md → src/elementary-number-theory/standard-cyclic-groups.lagda.md

@@ -1,7 +1,7 @@
-# The groups `ℤ/kℤ`
+# The standard cyclic groups
 
 ```agda
-module elementary-number-theory.groups-of-modular-arithmetic where
+module elementary-number-theory.standard-cyclic-groups where
 ```
 
 <details><summary>Imports</summary>
@@ -22,17 +22,29 @@ open import group-theory.semigroups
 
 ## Idea
 
-The integers modulo k, equipped with the zero-element, addition, and negatives,
-form groups.
+The **standard cyclic groups** are the [groups](group-theory.groups.md) of
+[integers](elementary-number-theory.integers.md)
+[modulo `k`](elementary-number-theory.modular-arithmetic.md). The standard
+cyclic groups are [abelian groups](group-theory.abelian-groups.md).
 
-## Definition
+The fact that the standard cyclic groups are
+[cyclic groups](group-theory.cyclic-groups.md) is shown in
+[`elementary-number-theory.standard-cyclic-rings`](elementary-number-theory.standard-cyclic-rings.md).
+
+## Definitions
+
+### The semigroup `ℤ/k`
 
 ```agda
 ℤ-Mod-Semigroup : (k : ℕ) → Semigroup lzero
 pr1 (ℤ-Mod-Semigroup k) = ℤ-Mod-Set k
 pr1 (pr2 (ℤ-Mod-Semigroup k)) = add-ℤ-Mod k
 pr2 (pr2 (ℤ-Mod-Semigroup k)) = associative-add-ℤ-Mod k
+```
 
+### The group `ℤ/k`
+
+```agda
 ℤ-Mod-Group : (k : ℕ) → Group lzero
 pr1 (ℤ-Mod-Group k) = ℤ-Mod-Semigroup k
 pr1 (pr1 (pr2 (ℤ-Mod-Group k))) = zero-ℤ-Mod k
@@ -41,8 +53,18 @@ pr2 (pr2 (pr1 (pr2 (ℤ-Mod-Group k)))) = right-unit-law-add-ℤ-Mod k
 pr1 (pr2 (pr2 (ℤ-Mod-Group k))) = neg-ℤ-Mod k
 pr1 (pr2 (pr2 (pr2 (ℤ-Mod-Group k)))) = left-inverse-law-add-ℤ-Mod k
 pr2 (pr2 (pr2 (pr2 (ℤ-Mod-Group k)))) = right-inverse-law-add-ℤ-Mod k
+```
 
+### The abelian group `ℤ/k`
+
+```agda
 ℤ-Mod-Ab : (k : ℕ) → Ab lzero
 pr1 (ℤ-Mod-Ab k) = ℤ-Mod-Group k
 pr2 (ℤ-Mod-Ab k) = commutative-add-ℤ-Mod k
 ```
+
+## See also
+
+### Table of files related to cyclic types, groups, and rings
+
+{{#include tables/cyclic-types.md}}