Refactor elementary number theory

references.bib

@@ -1,4 +1,4 @@
-@online{1000+theorems,
+G@online{1000+theorems,
   title  = {1000+ theorems},
   author = {Freek Wiedijk},
   url    = {https://1000-plus.github.io/}
@@ -10,6 +10,16 @@ @online{100theorems
   url    = {https://www.cs.ru.nl/~freek/100/}
 }
 
+@book{AZ18,
+  author      = {Aigner, Martin and Ziegler, G\"{u}nter M.},
+  title       = {Proofs from THE BOOK},
+  year        = {2018},
+  isbn        = {3662572648},
+  publisher   = {Springer Publishing Company, Incorporated},
+  edition     = {6th},
+  abstract    = {This revised and enlarged sixth edition of Proofs from THE BOOKfeatures an entirely new chapter on Van der Waerdens permanent conjecture, as well as additional, highly original and delightful proofs in other chapters.}
+}
+
 @article{AKS15,
   title       = {Univalent Categories and the {{Rezk}} Completion},
   author      = {Ahrens, Benedikt and Kapulkin, Krzysztof and Shulman, Michael},
@@ -54,6 +64,16 @@ @article{AL19
   langid      = {english}
 }
 
+@book{Andrews94,
+  title       = {Number Theory},
+  author      = {Andrews, G.E.},
+  isbn        = {9780486682525},
+  lccn        = {lc94005243},
+  series      = {Dover Books on Mathematics},
+  year        = {1994},
+  publisher   = {Dover Publications}
+}
+
 @misc{Awodey22,
        author = {{Awodey}, Steve},
         title = "{On Hofmann-Streicher universes}",
@@ -335,6 +355,15 @@ @article{Esc21
   keywords     = {55U40 03B15,Mathematics - Algebraic Geometry,Mathematics - Logic}
 }
 
+@book{Euler1748,
+  author       = {Leonhard Euler},
+  title        = {Introductio in analysin infinitorum},
+  year         = {1748},
+  publisher    = {Typographia Academiae Imperialis Petropolitanae},
+  url          = {https://archive.org/details/introductioanaly00eule_0},
+  note         = {Accessed: 2025-01-20}
+}
+
 @book{FBL73,
   author    = {Fraenkel, Abraham A. and Bar-Hillel, Yehoshua and Levy,
                Azriel},
@@ -358,6 +387,14 @@ @online{Felixwellen/DCHoTT-Agda
   howpublished = {{{GitHub}} repository}
 }
 
+@misc{Fibonacci1202,
+  author       = {Fibonacci},
+  title        = {Liber Abaci},
+  year         = {1202},
+  note         = {A scanned copy of Fibonacci's *Liber Abaci* is available through the Linda Hall Library Digital Collections.},
+  url          = {https://old.maa.org/press/periodicals/convergence/mathematical-treasure-fibonacci-s-liber-abaci}
+}
+
 @online{GGMS24,
   title       = {The {{Category}} of {{Iterative Sets}} in {{Homotopy Type Theory}} and {{Univalent Foundations}}},
   author      = {Gratzer, Daniel and Gylterud, Håkon and Mörtberg, Anders and Stenholm, Elisabeth},
@@ -372,6 +409,16 @@ @online{GGMS24
   keywords    = {Computer Science - Logic in Computer Science,Mathematics - Logic}
 }
 
+@book{HW08,
+  title       = {{An Introduction to the Theory of Numbers (6th edition)}},
+  author      = {Hardy, G. H. and Wright, Edward M. and Heath-Brown, D. R. and Silverman, Joseph H.},
+  isbn        = {0199219869},
+  keywords    = {congruences, primitive roots, residue systems, instructional exposition},
+  publisher   = {Oxford University Press},
+  year        = {2008},
+  abstract    = {{The sixth edition of the classic undergraduate text in elementary number theory includes a new chapter on elliptic curves and their role in the proof of Fermat's Last Theorem, a foreword by Andrew Wiles and extensively revised and updated end-of-chapter notes.}},
+}
+
 @article{KECA17,
   title       = {{Notions of Anonymous Existence in {{Martin-L\"of}} Type Theory}},
   author      = {Nicolai Kraus and Martín Escardó and Thierry Coquand and Thorsten Altenkirch},
@@ -415,6 +462,41 @@ @inproceedings{KvR19
   eprintclass = {cs, math}
 }
 
+@book{Leibniz1693,
+  author      = {Gottfried Wilhelm Leibniz},
+  title       = {De geometria analysis},
+  year        = {1693},
+  publisher   = {Leibniz's own press, Vienna},
+  note        = {This text is often cited as one of Leibniz's early works on calculus.}
+}
+
+@book{Leveque12volI,
+  title       = {Topics in Number Theory, Volume I},
+  author      = {LeVeque, W.J.},
+  isbn        = {9780486152080},
+  series      = {Dover Books on Mathematics},
+  year        = {2012},
+  publisher   = {Dover Publications}
+}
+
+@book{Leveque12volII,
+  title       = {Topics in Number Theory, Volume II},
+  author      = {LeVeque, W.J.},
+  isbn        = {9780486152080},
+  series      = {Dover Books on Mathematics},
+  year        = {2012},
+  publisher   = {Dover Publications}
+}
+
+@book{lucas1891,
+  title = {Théorie des Nombres},
+  author = {Lucas, Édouard},
+  year = {1891},
+  publisher = {Gauthier-Villars},
+  address = {Paris},
+  url = {https://archive.org/details/thoriedesnombr01lucauoft}
+}
+
 @incollection{Makkai98,
   author     = {Makkai, M.},
   title      = {Towards a categorical foundation of mathematics},
@@ -560,6 +642,18 @@ @misc{Mye21
   primaryclass  = {math.CT}
 }
 
+@book {NZM,
+  author      = {Niven, Ivan and Zuckerman, Herbert S. and Montgomery, Hugh L.},
+  title       = {An introduction to the theory of numbers},
+  edition     = {Fifth},
+  publisher   = {John Wiley \& Sons, Inc., New York},
+  year        = {1991},
+  pages       = {xiv+529},
+  isbn        = {0-471-62546-9},
+  mrclass     = {11-01},
+  mrnumber    = {1083765},
+}
+
 @online{oeis,
   title        = {The {{On-Line Encyclopedia}} of {{Integer Sequences}}},
   author       = {OEIS Foundation Inc.},
@@ -583,6 +677,15 @@ @phdthesis{Qui16
   langid = {english}
 }
 
+@book{Recorde1557,
+  author    = {Robert Recorde},
+  title     = {The Whetstone of Witte},
+  year      = {1557},
+  publisher = {Printed by John Daye, London},
+  note      = {This work contains the first recorded use of the equals sign (=).},
+  url       = {https://archive.org/embed/TheWhetstoneOfWitte}
+}
+
 @book{Rie17,
   title     = {Category {{Theory}} in {{Context}}},
   author    = {Riehl, Emily},
@@ -890,3 +993,14 @@ @online{Warn24
   pubstate    = {preprint},
   keywords    = {Mathematics - Algebraic Topology,Mathematics - Category Theory}
 }
+
+@book{Widmann1489,
+  author      = {Johannes Widmann},
+  title       = {Behende und hüpsche Rechenung auff allen Kauffmanschafft},
+  year        = {1489},
+  publisher   = {Conrad Kachelofen},
+  address     = {Leipzig},
+  note        = {First use of "+" and "−" symbols in printed mathematics},
+  language    = {German},
+  url         = {https://www.loc.gov/item/49038907}
+}

src/commutative-algebra/groups-of-units-commutative-rings.lagda.md

@@ -11,6 +11,7 @@ open import category-theory.functors-large-precategories
 
 open import commutative-algebra.commutative-rings
 open import commutative-algebra.homomorphisms-commutative-rings
+open import commutative-algebra.invertible-elements-commutative-rings
 open import commutative-algebra.precategory-of-commutative-rings
 
 open import foundation.dependent-pair-types
@@ -35,8 +36,9 @@ open import ring-theory.groups-of-units-rings
 
 ## Idea
 
-The **group of units** of a
-[commutative ring](commutative-algebra.commutative-rings.md) `A` is the
+The
+{{#concept "group of units" Disambiguation="commutative ring" WD="unit" WDID=Q118084}}
+of a [commutative ring](commutative-algebra.commutative-rings.md) `A` is the
 [abelian group](group-theory.abelian-groups.md) consisting of all the
 [invertible elements](commutative-algebra.invertible-elements-commutative-rings.md)
 in `A`. Equivalently, the group of units of `A` is the
@@ -177,6 +179,14 @@ module _
   inclusion-group-of-units-Commutative-Ring =
     inclusion-group-of-units-Ring (ring-Commutative-Ring A)
 
+  is-invertible-element-inclusion-group-of-units-Commutative-Ring :
+    (x : type-group-of-units-Commutative-Ring) →
+    is-invertible-element-Commutative-Ring A
+      ( inclusion-group-of-units-Commutative-Ring x)
+  is-invertible-element-inclusion-group-of-units-Commutative-Ring =
+    is-invertible-element-inclusion-group-of-units-Ring
+      ( ring-Commutative-Ring A)
+
   preserves-mul-inclusion-group-of-units-Commutative-Ring :
     {x y : type-group-of-units-Commutative-Ring} →
     inclusion-group-of-units-Commutative-Ring
@@ -324,3 +334,22 @@ preserves-id-functor-Large-Precategory
   group-of-units-commutative-ring-functor-Large-Precategory {X = A} =
   preserves-id-hom-group-of-units-hom-Commutative-Ring A
 ```
+
+### Negatives of units
+
+```agda
+module _
+  {l : Level} (A : Commutative-Ring l)
+  where
+
+  neg-group-of-units-Commutative-Ring :
+    type-group-of-units-Commutative-Ring A →
+    type-group-of-units-Commutative-Ring A
+  neg-group-of-units-Commutative-Ring =
+    neg-group-of-units-Ring (ring-Commutative-Ring A)
+
+  neg-unit-group-of-units-Commutative-Ring :
+    type-group-of-units-Commutative-Ring A
+  neg-unit-group-of-units-Commutative-Ring =
+    neg-unit-group-of-units-Ring (ring-Commutative-Ring A)
+```

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

@@ -9,6 +9,7 @@ module commutative-algebra.invertible-elements-commutative-rings where
 ```agda
 open import commutative-algebra.commutative-rings
 
+open import foundation.action-on-identifications-functions
 open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.identity-types
@@ -70,7 +71,7 @@ module _
       ( ring-Commutative-Ring A)
 ```
 
-### Aight invertible elements of commutative rings
+### Right invertible elements of commutative rings
 
 ```agda
 module _
@@ -241,7 +242,7 @@ module _
     is-invertible-element-inverse-Ring (ring-Commutative-Ring A)
 ```
 
-### Any invertible element of a monoid has a contractible type of right inverses
+### Any invertible element of a commutative ring has a contractible type of right inverses
 
 ```agda
 module _
@@ -255,7 +256,7 @@ module _
     is-contr-is-right-invertible-element-Ring (ring-Commutative-Ring A)
 ```
 
-### Any invertible element of a monoid has a contractible type of left inverses
+### Any invertible element of a commutative ring has a contractible type of left inverses
 
 ```agda
 module _
@@ -269,7 +270,7 @@ module _
     is-contr-is-left-invertible-Ring (ring-Commutative-Ring A)
 ```
 
-### The unit of a monoid is invertible
+### The unit of a commutative ring is invertible
 
 ```agda
 module _
@@ -290,9 +291,17 @@ module _
     is-invertible-element-Commutative-Ring A (one-Commutative-Ring A)
   is-invertible-element-one-Commutative-Ring =
     is-invertible-element-one-Ring (ring-Commutative-Ring A)
+
+  is-invertible-element-is-one-Commutative-Ring :
+    (x : type-Commutative-Ring A) → one-Commutative-Ring A ＝ x →
+    is-invertible-element-Commutative-Ring A x
+  is-invertible-element-is-one-Commutative-Ring =
+    is-invertible-element-is-one-Ring (ring-Commutative-Ring A)
 ```
 
-### Invertible elements are closed under multiplication
+### A product `xy` is invertible if and only if both `x` and `y` are invertible
+
+#### Invertible elements are closed under multiplication
 
 ```agda
 module _
@@ -324,6 +333,46 @@ module _
     is-invertible-element-mul-Ring (ring-Commutative-Ring A)
 ```
 
+#### If `xy` is invertible then so is `x`
+
+```agda
+module _
+  {l : Level} (A : Commutative-Ring l) (x y : type-Commutative-Ring A)
+  where
+
+  is-invertible-element-left-factor-Commutative-Ring :
+    is-invertible-element-Commutative-Ring A (mul-Commutative-Ring A x y) →
+    is-invertible-element-Commutative-Ring A x
+  pr1 (is-invertible-element-left-factor-Commutative-Ring (u , p , q)) =
+    mul-Commutative-Ring A y u
+  pr1 (pr2 (is-invertible-element-left-factor-Commutative-Ring (u , p , q))) =
+    inv (associative-mul-Commutative-Ring A x y u) ∙ p
+  pr2 (pr2 (is-invertible-element-left-factor-Commutative-Ring (u , p , q))) =
+    right-swap-mul-Commutative-Ring A y u x ∙
+    ap (mul-Commutative-Ring' A u) (commutative-mul-Commutative-Ring A y x) ∙
+    p
+```
+
+#### If `xy` is invertible then so is `y`
+
+```agda
+module _
+  {l : Level} (A : Commutative-Ring l) (x y : type-Commutative-Ring A)
+  where
+
+  is-invertible-element-right-factor-Commutative-Ring :
+    is-invertible-element-Commutative-Ring A (mul-Commutative-Ring A x y) →
+    is-invertible-element-Commutative-Ring A y
+  pr1 (is-invertible-element-right-factor-Commutative-Ring (u , p , q)) =
+    mul-Commutative-Ring A u x
+  pr1 (pr2 (is-invertible-element-right-factor-Commutative-Ring (u , p , q))) =
+    left-swap-mul-Commutative-Ring A y u x ∙
+    ap (mul-Commutative-Ring A u) (commutative-mul-Commutative-Ring A y x) ∙
+    q
+  pr2 (pr2 (is-invertible-element-right-factor-Commutative-Ring (u , p , q))) =
+    associative-mul-Commutative-Ring A u x y ∙ q
+```
+
 ### The inverse of an invertible element is invertible
 
 ```agda