exists_SL2_col — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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