exists_SL2_row — Mathlib

English

Given coprime a,b in R, there exists g ∈ SL(2,R) with g(i,0) = a and g(i,1) = b for i ∈ Fin 2.

Русский

Для любых взаимно простых a,b существует g ∈ SL(2,R) с g(i,0) = a, g(i,1) = b для i ∈ Fin 2.

LaTeX

$$∃ g : SL(2,R), g i 0 = a ∧ g i 1 = b$$

Lean4

/-- Given any pair of coprime elements of `R`, there exists a matrix in `SL(2, R)` having those
entries as its top or bottom row. -/
theorem exists_SL2_row {a b : R} (hab : IsCoprime a b) (i : Fin 2) : ∃ g : SL(2, R), g i 0 = a ∧ g i 1 = b :=
  by
  obtain ⟨u, v, h⟩ := hab
  refine
      match i with
      | 0 => ⟨⟨!![a, b; -v, u], ?_⟩, rfl, rfl⟩
      | 1 => ⟨⟨!![v, -u; a, b], ?_⟩, rfl, rfl⟩ <;>
    · rw [Matrix.det_fin_two_of, ← h]
      ring

Похожие утверждения