Euclidean algorithm — flashcards
Every card the map can derive about Euclidean algorithm — definitions, statements, attribution, and the edges it sits on.
Theorems 6
State: The Euclidean algorithm terminates.
For positive integers a and b, the remainder sequence is strictly decreasing and non-negative, so it reaches zero after finitely many steps.
derived from st/euclid-terminates by the statement rule
State: Bézout's identity.
For integers a, b there exist integers x, y with ax + by = gcd(a, b). The extended Euclidean algorithm computes them.
derived from st/bezout by the statement rule
State: Lamé's theorem.
The number of division steps in the Euclidean algorithm is at most five times the number of decimal digits of the smaller argument; the worst case is consecutive Fibonacci numbers.
derived from st/lame by the statement rule
State: √2 is irrational.
Anthyphairesis on a 1 by √2 rectangle never terminates, which is exactly the statement that √2 is not a ratio of integers.
derived from st/sqrt2-irrational by the statement rule
State: Hensel's lemma.
If f(a) ≡ 0 mod p and f'(a) ≢ 0 mod p, then f has a unique p-adic root congruent to a. It is Newton's method with the ultrametric inequality doing the work that real-analytic estimates do over ℝ.
derived from st/hensel by the statement rule
State: Hensel's lemma, sharp form.
If |f(a)|_p < |f′(a)|_p² then f has a unique root α with |α − a|_p < |f′(a)|_p. Dropping the requirement that a be a simple root mod p is what makes the lemma usable in practice.
derived from st/hensel-general by the statement rule
Names and dates 6
The Euclidean algorithm terminates — who, and when?
Euclid, c. 300 BC.
derived from st/euclid-terminates by the attribution rule
Bézout's identity — who, and when?
Claude Bachet, then Étienne Bézout, 1624 (Bachet), 1779 (Bézout).
derived from st/bezout by the attribution rule
Lamé's theorem — who, and when?
Gabriel Lamé, 1844.
derived from st/lame by the attribution rule
√2 is irrational — who, and when?
the Pythagorean school, c. 450 BC.
derived from st/sqrt2-irrational by the attribution rule
Hensel's lemma — who, and when?
Kurt Hensel, 1897.
derived from st/hensel by the attribution rule
Hensel's lemma, sharp form — who, and when?
Hasse, Schnirelmann, Teichmüller and others, 1920s–1930s.
derived from st/hensel-general by the attribution rule
Formalisation 3
What is Bézout's identity called in Mathlib?
Nat.gcd_eq_gcd_ab — Mathlib.Data.Int.GCD
derived from st/bezout by the binding rule
What is √2 is irrational called in Mathlib?
irrational_sqrt_two — Mathlib.NumberTheory.Real.Irrational
derived from st/sqrt2-irrational by the binding rule
What is Hensel's lemma, sharp form called in Mathlib?
hensels_lemma — Mathlib.NumberTheory.Padics.Hensel
derived from st/hensel-general by the binding rule
Connections 5
Under the Information cost lens, how do Euclidean algorithm and Continued fractions relate? [Information cost]
The continued fraction of x is the quotient sequence of the Euclidean algorithm run on x. Identical work; the CF keeps only the quotients and discards the remainders, which is exactly where the magnitude information lived.
derived from information-cost:euclidean-algorithm→continued-fractions by the connection rule
Between Euclidean algorithm and Continued fractions, which way does the reasoning actually run? [Direction]
Euclid's algorithm consumes a pair and reduces it; the continued fraction it produces generates approximations outward. The same recursion read as destruction or as construction depending on which end you stand at.
derived from direction:euclidean-algorithm→continued-fractions by the connection rule
In Mathlib, what is the import relation between p-adic numbers and Euclidean algorithm? [Dependency (Mathlib)]
`Mathlib.NumberTheory.Padics.PadicVal.Basic` imports `Mathlib.NumberTheory.Divisors`. Read off Mathlib/NumberTheory/Padics/PadicVal/Basic.html. No human asserted this edge.
derived from dependency:p-adic-numbers→euclidean-algorithm by the connection rule
In Mathlib, what is the import relation between Euclidean algorithm and Rings & fields? [Dependency (Mathlib)]
`Mathlib.Data.Int.GCD` imports `Mathlib.Algebra.Divisibility.Basic`, `Mathlib.Algebra.GroupWithZero.Semiconj`, `Mathlib.Algebra.GroupWithZero.Divisibility`, `Mathlib.Algebra.GroupWithZero.Nat`. Read off Mathlib/Data/Int/GCD.html. No human asserted this edge.
derived from dependency:euclidean-algorithm→rings-fields by the connection rule
In Mathlib, what is the import relation between Euclidean algorithm and Groups & symmetry? [Dependency (Mathlib)]
`Mathlib.Data.Int.GCD` imports `Mathlib.Algebra.Group.Commute.Units`, `Mathlib.Algebra.Group.Int.Defs`, `Mathlib.Algebra.Group.Nat.Defs`, `Mathlib.Algebra.Group.Nat.Units`. Read off Mathlib/Data/Int/GCD.html. No human asserted this edge.
derived from dependency:euclidean-algorithm→group-theory by the connection rule
Concepts 1
What is Euclidean algorithm, in one sentence?
Repeated division to find the gcd of two numbers — the oldest algorithm still in everyday use.
derived from euclidean-algorithm by the concept rule