lean_workbook_plus_14263

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Given $m|n^a+1$ and $m|n^b+1$ , prove that $m$ divides $gcd(n^a+1, n^b+1)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14263 {m n a b : ℕ} (hm : m ∣ n^a + 1) (hn : m ∣ n^b + 1) : m ∣ Nat.gcd (n^a + 1) (n^b + 1)   :=  by sorry

Source