English
For every coprime pair (c,d) ∈ ℤ^2 with gcd(c,d)=1 there exists a matrix g ∈ SL(2,ℤ) whose bottom row is (c,d). In other words, every coprime pair appears as the bottom row of some unimodular 2×2 integer matrix.
Русский
Для каждой пары целых чисел (c,d) с gcd(c,d)=1 существует матрица g ∈ SL(2,ℤ), чья нижняя строка равна (c,d). Другими словами, любая взаимно простая пара является нижней строкой некоторой unimodularной матрицы 2×2 над целыми.
LaTeX
$$$\\forall (c,d) \\in \\mathbb{Z}^2,\\; \\gcd(c,d)=1 \\ \\Rightarrow\\ \\exists g \\in SL(2,\\mathbb{Z})\\text{ such that the bottom row of } g \\text{ is } (c,d).$$$
Lean4
/-- Every pair `![c, d]` of coprime integers is the "bottom_row" of some element `g=[[*,*],[c,d]]`
of `SL(2,ℤ)`. -/
theorem bottom_row_surj {R : Type*} [CommRing R] :
Set.SurjOn (fun g : SL(2, R) => (↑g : Matrix (Fin 2) (Fin 2) R) 1) Set.univ {cd | IsCoprime (cd 0) (cd 1)} :=
by
rintro cd ⟨b₀, a, gcd_eqn⟩
let A := of ![![a, -b₀], cd]
have det_A_1 : det A = 1 := by
convert gcd_eqn
rw [det_fin_two]
simp [A, (by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]
refine ⟨⟨A, det_A_1⟩, Set.mem_univ _, ?_⟩
ext; simp [A]
