isCoprime_col — Mathlib

English

For any A ∈ SL(2,R) and j ∈ Fin 2, the pair (A(0,j), A(1,j)) is coprime.

Русский

Для любого A ∈ SL(2,R) и j ∈ Fin 2, пара (A(0,j), A(1,j)) взаимно простая.

LaTeX

$$IsCoprime (A.0 j) (A.1 j)$$

Lean4

theorem isCoprime_col (A : SL(2, R)) (j : Fin 2) : IsCoprime (A 0 j) (A 1 j) := by
  refine
      match j with
      | 0 => ⟨A 1 1, -(A 0 1), ?_⟩
      | 1 => ⟨-(A 1 0), A 0 0, ?_⟩ <;>
    · simp_rw [det_coe A ▸ det_fin_two A.1]
      ring

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