fermat_catalan.variants.darmon_granville

By the **Darmon-Granville** theorem, for any fixed choice of positive integers m, n and k satisfying $\frac 1 m + \frac 1 n + \frac 1 k < 1$, only finitely many coprime triples $(a, b, c)$ solving $a^m + b^n = c^k$ exist.

theorem fermat_catalan.variants.darmon_granville
    (m n k : ℕ) (hm : 0 < m) (hn : 0 < n) (hk : 0 < k)
    (H : (1 / m : ℝ) + 1 / n + 1 / k < 1) :
    {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ a^m + b^n = c^k ∧
      ({a, b, c} : Set _).Pairwise Nat.Coprime}.Finite

Recent Submissions

No submissions yet. Be the first to attempt this problem.