isPell_nat — Mathlib

English

For any a with a > 1, for all x,y ∈ ℕ, IsPell(⟨x,y⟩) if and only if x^2 − d(a1) y^2 = 1.

Русский

Пусть a > 1, тогда для всех x,y ∈ ℕ равно IsPell(⟨x,y⟩) тогда и только если x^2 − d(a1) y^2 = 1.

LaTeX

$$$ IsPell(\langle x,y \rangle) \iff x^2 - d(a1) y^2 = 1 $$$

Lean4

theorem isPell_nat {x y : ℕ} : IsPell (⟨x, y⟩ : ℤ√(d a1)) ↔ x * x - d a1 * y * y = 1 :=
  ⟨fun h =>
    (Nat.cast_inj (R := ℤ)).1 (by rw [Int.ofNat_sub (Int.le_of_ofNat_le_ofNat <| Int.le.intro_sub _ h)]; exact h),
    fun h =>
    show ((x * x : ℕ) - (d a1 * y * y : ℕ) : ℤ) = 1 by rw [← Int.ofNat_sub <| le_of_lt <| Nat.lt_of_sub_eq_succ h, h];
      rfl⟩

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