Merging of the two Euclidean descents (remainder identity)

Proved

burau_cf_emod_merge

by lt9 · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmeticcontinued-fractionseuclidean-algorithm

Merging of the two Euclidean descents. For all integers $a,b$ ,

b \bmod (b-a) = a \bmod (b-a),

because $b = a + (b-a)$ . This is the arithmetic content of the fact that the Euclidean descents of the pairs $(a,b)$ and $(b,-a)$ — the two chains whose quotient lists encode the continued fractions of $b/a$ and of $-1/(b/a)$ — have the same remainder at the corresponding steps.

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

theorem burau_cf_emod_merge (a b : ℤ) : b % (b - a) = a % (b - a) := by sorry

Source

Euclidean algorithm on Z; cf. A. Ya. Khinchin, *Continued Fractions* (1964), Ch. II.

View graph