Skip to content

Commit 00371f3

Browse files
Bezout's lemma – 100 theorems (#1202)
Turns out I missed a few results. --------- Co-authored-by: Egbert Rijke <e.m.rijke@gmail.com>
1 parent 346e0c1 commit 00371f3

File tree

1 file changed

+13
-0
lines changed

1 file changed

+13
-0
lines changed

src/literature/100-theorems.lagda.md

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,19 @@ open import elementary-number-theory.binomial-theorem-natural-numbers using
5454

5555
> This is not yet formalized.
5656
57+
### [60. Bezout's Lemma](https://www.cs.ru.nl/~freek/100/#60) {#60}
58+
59+
Note that the 60th theorem in Freek's list is listed as "Bezout's Theorem",
60+
while the linked theorems are formalizations of Bezout's lemma, even though
61+
these are different statements.
62+
63+
```agda
64+
open import elementary-number-theory.bezouts-lemma-integers using
65+
( bezouts-lemma-ℤ)
66+
open import elementary-number-theory.bezouts-lemma-natural-numbers using
67+
( bezouts-lemma-ℕ)
68+
```
69+
5770
### [63. Cantor's Theorem](https://www.cs.ru.nl/~freek/100/#63) {#63}
5871

5972
```agda

0 commit comments

Comments
 (0)