isCoprime_row — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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