theorem
proved
fermat_one
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 1259.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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. -/
1282theorem cousin_prime_nineteen_twentythree : Prime 19 ∧ Prime 23 ∧ 23 = 19 + 4 := by native_decide
1283
1284/-- 37 and 41 are cousin primes. -/
1285theorem cousin_prime_thirtyseven_fortyone : Prime 37 ∧ Prime 41 ∧ 41 = 37 + 4 := by native_decide
1286
1287/-- 43 and 47 are cousin primes. -/
1288theorem cousin_prime_fortythree_fortyseven : Prime 43 ∧ Prime 47 ∧ 47 = 43 + 4 := by native_decide
1289