vecMulSL — Mathlib

English

If v = (v0, v1) has coprime entries and A ∈ SL(2,R), then the vector v multiplied by A on the right has coprime coordinates.

Русский

Если v = (v0, v1) с взаимно простыми компонентами и A ∈ SL(2,R), то v A имеет взаимно простые координаты.

LaTeX

$$IsCoprime ( (v 0) * A.-? ) ( (v 1) * A.-? )$$

Lean4

/-- A vector with coprime entries, right-multiplied by a matrix in `SL(2, R)`, has
coprime entries. -/
theorem vecMulSL {v : Fin 2 → R} (hab : IsCoprime (v 0) (v 1)) (A : SL(2, R)) :
    IsCoprime ((v ᵥ* A.1) 0) ((v ᵥ* A.1) 1) :=
  by
  obtain ⟨g, hg⟩ := hab.exists_SL2_row 0
  have : v = g 0 :=
    funext fun t ↦ by { fin_cases t <;> tauto
    }
  simpa only [this] using isCoprime_row (g * A) 0

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