eq_pellZd — Mathlib

English

For a > 1 and b ∈ Z√d with b ≥ 1, IsPell b implies there exists n with b = pellZd a1 n.

Русский

Для a > 1 и b ∈ Z√d, если b ≥ 1 и IsPell b, то существует n, такое что b = pellZd a1 n.

LaTeX

$$$ \forall b\ (b \ge 1),\ IsPell(b) \Rightarrow \exists n\, b = pellZd(a1, n) $$$

Lean4

theorem eq_pellZd (b : ℤ√(d a1)) (b1 : 1 ≤ b) (hp : IsPell b) : ∃ n, b = pellZd a1 n :=
  let ⟨n, h⟩ := @Zsqrtd.le_arch (d a1) b
  eq_pell_lem a1 n b b1 hp <|
    h.trans <| by
      rw [Zsqrtd.natCast_val]
      exact Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| le_of_lt <| n_lt_xn _ _) (Int.ofNat_zero_le _)

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