Primes_of_form_Power_Less_One
Provedmersenne-primesprime-numbersproofwiki
Let m, n be positive natural numbers. If m^n - 1 is prime, then m = 2 and n is prime.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Prime.Basic
Formal statement
theorem Primes_of_form_Power_Less_One (m n : ℕ) (hm : m > 1) (hn : n > 1) (hp : Nat.Prime (m ^ n - 1)) : m = 2 ∧ Nat.Prime n := by sorry
Source