Bezout's lemma – 100 theorems (#1202)

Turns out I missed a few results. --------- Co-authored-by: Egbert Rijke <[email protected]>
UniMath · Oct 18, 2024 · 00371f3 · 00371f3
1 parent 346e0c1
commit 00371f3
Showing 1 changed file with 13 additions and 0 deletions.
diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md
@@ -54,6 +54,19 @@ open import elementary-number-theory.binomial-theorem-natural-numbers using
 
 > This is not yet formalized.
 
+### [60. Bezout's Lemma](https://www.cs.ru.nl/~freek/100/#60) {#60}
+
+Note that the 60th theorem in Freek's list is listed as "Bezout's Theorem",
+while the linked theorems are formalizations of Bezout's lemma, even though
+these are different statements.
+
+```agda
+open import elementary-number-theory.bezouts-lemma-integers using
+  ( bezouts-lemma-ℤ)
+open import elementary-number-theory.bezouts-lemma-natural-numbers using
+  ( bezouts-lemma-ℕ)
+```
+
 ### [63. Cantor's Theorem](https://www.cs.ru.nl/~freek/100/#63) {#63}
 
 ```agda