From 00371f3d6d5777611c3c3255eab36895712341af Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Fri, 18 Oct 2024 19:26:50 +0200 Subject: [PATCH] =?UTF-8?q?Bezout's=20lemma=20=E2=80=93=20100=20theorems?= =?UTF-8?q?=20(#1202)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Turns out I missed a few results. --------- Co-authored-by: Egbert Rijke --- src/literature/100-theorems.lagda.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/literature/100-theorems.lagda.md b/src/literature/100-theorems.lagda.md index 7c4f1b1958..a193a72d76 100644 --- 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