@[simp]
@[simp]
theorem
pell.is_pell_mul
{a : ℕ}
(a1 : 1 < a)
{b c : ℤ√↑(d a1)} :
pell.is_pell a1 b → pell.is_pell a1 c → pell.is_pell a1 (b * c)
theorem
pell.is_pell_conj
{a : ℕ}
(a1 : 1 < a)
{b : ℤ√↑(d a1)} :
pell.is_pell a1 b ↔ pell.is_pell a1 b.conj
@[simp]
theorem
pell.pell_zd_succ
{a : ℕ}
(a1 : 1 < a)
(n : ℕ) :
pell.pell_zd a1 (n + 1) = pell.pell_zd a1 n * {re := ↑a, im := 1}
theorem
pell.eq_pell_lem
{a : ℕ}
(a1 : 1 < a)
(n : ℕ)
(b : ℤ√↑(d a1)) :
1 ≤ b → pell.is_pell a1 b → b ≤ pell.pell_zd a1 n → (∃ (n : ℕ), b = pell.pell_zd a1 n)
theorem
pell.eq_pell_zd
{a : ℕ}
(a1 : 1 < a)
(b : ℤ√↑(d a1)) :
1 ≤ b → pell.is_pell a1 b → (∃ (n : ℕ), b = pell.pell_zd a1 n)
theorem
pell.pell_zd_add
{a : ℕ}
(a1 : 1 < a)
(m n : ℕ) :
pell.pell_zd a1 (m + n) = pell.pell_zd a1 m * pell.pell_zd a1 n
theorem
pell.pell_zd_sub
{a : ℕ}
(a1 : 1 < a)
{m n : ℕ} :
n ≤ m → pell.pell_zd a1 (m - n) = pell.pell_zd a1 m * (pell.pell_zd a1 n).conj
theorem
pell.pell_zd_succ_succ
{a : ℕ}
(a1 : 1 < a)
(n : ℕ) :
pell.pell_zd a1 (n + 2) + pell.pell_zd a1 n = ↑(2 * a) * pell.pell_zd a1 (n + 1)
theorem
pell.matiyasevic
{a k x y : ℕ} :
(∃ (a1 : 1 < a), pell.xn a1 k = x ∧ pell.yn a1 k = y) ↔ 1 < a ∧ k ≤ y ∧ (x = 1 ∧ y = 0 ∨ ∃ (u v s t b : ℕ), x * x - (a * a - 1) * y * y = 1 ∧ u * u - (a * a - 1) * v * v = 1 ∧ s * s - (b * b - 1) * t * t = 1 ∧ 1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])