bottom_row_coprime — Mathlib

English

For any g ∈ SL(2, R), the two bottom row entries are coprime.

Русский

Для любого g ∈ SL(2, R) два элемента нижней строки взаимно просты.

LaTeX

$$$\gcd(g_{1,0}, g_{1,1}) = 1$$$

Lean4

/-- The two numbers `c`, `d` in the "bottom_row" of `g=[[*,*],[c,d]]` in `SL(2, ℤ)` are coprime. -/
theorem bottom_row_coprime {R : Type*} [CommRing R] (g : SL(2, R)) :
    IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1) :=
  isCoprime_row g 1

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