pell_eq — Mathlib

English

For all a with a > 1 and n, x_n(a1,n)^2 − d(a1) y_n(a1,n)^2 = 1.

Русский

Для всех a > 1 и n выполняется x_n(a1,n)^2 − d(a1) y_n(a1,n)^2 = 1.

LaTeX

$$$ x_n(a1,n)^2 - d(a1)\, y_n(a1,n)^2 = 1 $$$

Lean4

@[simp]
theorem pell_eq (n : ℕ) : xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n = 1 :=
  let pn := pell_eqz a1 n
  have h : (↑(xn a1 n * xn a1 n) : ℤ) - ↑(d a1 * yn a1 n * yn a1 n) = 1 := by repeat' rw [Int.natCast_mul]; exact pn
  have hl : d a1 * yn a1 n * yn a1 n ≤ xn a1 n * xn a1 n :=
    Nat.cast_le.1 <| Int.le.intro _ <| add_eq_of_eq_sub' <| Eq.symm h
  (Nat.cast_inj (R := ℤ)).1 (by rw [Int.ofNat_sub hl]; exact h)

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