xy_coprime — Mathlib

English

For a > 1 and any n, gcd(x_n(a), y_n(a)) = 1; i.e., x_n(a) and y_n(a) are coprime.

Русский

Для a > 1 и любого n, gcd(x_n(a), y_n(a)) = 1; то есть x_n(a) и y_n(a) взаимно просты.

LaTeX

$$$\\gcd\\big(x^{(a)}_{n}, y^{(a)}_{n}\\big) = 1.$$$

Lean4

theorem xy_coprime (n) : (xn a1 n).Coprime (yn a1 n) :=
  Nat.coprime_of_dvd' fun k _ kx ky => by
    let p := pell_eq a1 n
    rw [← p]
    exact Nat.dvd_sub (kx.mul_left _) (ky.mul_left _)

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