theorem
proved
mersenne_seven
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1251.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1248theorem mersenne_five : Prime (2 ^ 5 - 1) := by native_decide
1249
1250/-- 2^7 - 1 = 127 is a Mersenne prime. -/
1251theorem mersenne_seven : Prime (2 ^ 7 - 1) := by native_decide
1252
1253/-! ### Fermat primes (2^(2^n) + 1) -/
1254
1255/-- F_0 = 2^(2^0) + 1 = 3 is a Fermat prime. -/
1256theorem fermat_zero : Prime (2 ^ (2 ^ 0) + 1) := by native_decide
1257
1258/-- F_1 = 2^(2^1) + 1 = 5 is a Fermat prime. -/
1259theorem fermat_one : Prime (2 ^ (2 ^ 1) + 1) := by native_decide
1260
1261/-- F_2 = 2^(2^2) + 1 = 17 is a Fermat prime. -/
1262theorem fermat_two : Prime (2 ^ (2 ^ 2) + 1) := by native_decide
1263
1264/-- F_3 = 2^(2^3) + 1 = 257 is a Fermat prime. -/
1265theorem fermat_three : Prime (2 ^ (2 ^ 3) + 1) := by native_decide
1266
1267/-- F_4 = 2^(2^4) + 1 = 65537 is a Fermat prime. -/
1268theorem fermat_four : Prime (2 ^ (2 ^ 4) + 1) := by native_decide
1269
1270/-! ### Cousin primes (differ by 4) -/
1271
1272/-- 3 and 7 are cousin primes. -/
1273theorem cousin_prime_three_seven : Prime 3 ∧ Prime 7 ∧ 7 = 3 + 4 := by native_decide
1274
1275/-- 7 and 11 are cousin primes. -/
1276theorem cousin_prime_seven_eleven : Prime 7 ∧ Prime 11 ∧ 11 = 7 + 4 := by native_decide
1277
1278/-- 13 and 17 are cousin primes. -/
1279theorem cousin_prime_thirteen_seventeen : Prime 13 ∧ Prime 17 ∧ 17 = 13 + 4 := by native_decide
1280
1281/-- 19 and 23 are cousin primes. -/