Theorems · Theorem · number theory

Pell.matiyasevic

• 1000+ list: Matiyasevich's theorem

∀ {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])

Defined in

Mathlib.NumberTheory.PellMatiyasevic

Cited by

1 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound