Refactor elementary number theory

references.bib

@@ -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 BOOK features 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},
@@ -44,6 +54,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{Anel24,
   title         = {The category of $\pi$-finite spaces},
   author        = {Mathieu Anel},
@@ -66,16 +86,16 @@ @misc{Awodey22
 }
 
 @article{BauerTaylor2009,
-  author    = {Bauer, Andrej and Taylor, Paul},
-  title     = {The {D}edekind Reals in Abstract {S}tone Duality},
-  journal   = {Mathematical Structures in Computer Science},
-  publisher = {Cambridge University Press},
-  year      = 2009,
-  volume    = 19,
-  pages     = {757--838},
-  doi       = {10.1017/S0960129509007695},
-  url       = {PaulTaylor.EU/ASD/dedras/},
-  amsclass  = {03F60, 06E15, 18C20, 26E40, 54D45, 65G40}
+  author      = {Bauer, Andrej and Taylor, Paul},
+  title       = {The {D}edekind Reals in Abstract {S}tone Duality},
+  journal     = {Mathematical Structures in Computer Science},
+  publisher   = {Cambridge University Press},
+  year        = 2009,
+  volume      = 19,
+  pages       = {757--838},
+  doi         = {10.1017/S0960129509007695},
+  url         = {https://paultaylor.eu/ASD/dedras/},
+  amsclass    = {03F60, 06E15, 18C20, 26E40, 54D45, 65G40}
 }
 
 @online{BCDE21,
@@ -390,6 +410,15 @@ @article{Esc21b
   url           = {https://martinescardo.github.io/TypeTopology/InjectiveTypes.Article.html}
 }
 
+@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},
@@ -413,6 +442,28 @@ @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}
+}
+
+@book {Golan1999,
+  author     = {Golan, Jonathan S.},
+  title      = {Semirings and their applications},
+  publisher  = {Kluwer Academic Publishers, Dordrecht},
+  year       = {1999},
+  pages      = {xii+381},
+  isbn       = {0-7923-5786-8},
+  mrclass    = {16Y60 (68Q01)},
+  mrnumber   = {1746739},
+  mrreviewer = {Udo\ Hebisch},
+  doi        = {10.1007/978-94-015-9333-5},
+  url        = {https://doi.org/10.1007/978-94-015-9333-5},
+}
+
 @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},
@@ -427,6 +478,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},
@@ -479,6 +540,41 @@ @misc{Lavenir23
   primaryclass  = {math.AT}
 }
 
+@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},
@@ -608,6 +704,32 @@ @misc{Mye21
   primaryclass  = {math.CT}
 }
 
+@article {NoronhaGalvao1978,
+  author      = {{Noronha-Galv\~ao}, Maria Luísa},
+  title       = {Ideals in the semiring {$N$}},
+  journal     = {Portugal. Math.},
+  fjournal    = {Portugaliae Mathematica},
+  volume      = {37},
+  year        = {1978},
+  number      = {1-2},
+  pages       = {113--117},
+  issn        = {0032-5155,1662-2758},
+  mrclass     = {16A78 (20M25)},
+  mrnumber    = {620304},
+}
+
+@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.},
@@ -631,6 +753,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},
@@ -730,6 +861,18 @@ @article{RSS20
   keywords    = {Computer Science - Logic in Computer Science,F.3.1,F.3.1 F.4.1,F.4.1,Mathematics - Category Theory,Mathematics - Logic}
 }
 
+@article{Saidak2006,
+  author = {Saidak, Filip},
+  title = {A New Proof of Euclid's Theorem},
+  journal = {The American Mathematical Monthly},
+  volume = {113},
+  number = {10},
+  pages = {937--938},
+  year = {2006},
+  doi = {10.2307/27642094},
+  mrnumber = {2271540}
+}
+
 @online{Shu14SplittingIdempotents,
   title        = {Splitting {{Idempotents}}},
   author       = {Shulman, Mike},
@@ -938,3 +1081,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)
+```