theorem
proved
twin_prime_eleven_thirteen
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 1174.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1171theorem twin_prime_five_seven : Prime 5 ∧ Prime 7 ∧ 7 = 5 + 2 := by native_decide
1172
1173/-- 11 and 13 are twin primes. -/
1174theorem twin_prime_eleven_thirteen : Prime 11 ∧ Prime 13 ∧ 13 = 11 + 2 := by native_decide
1175
1176/-- 17 and 19 are twin primes. -/
1177theorem twin_prime_seventeen_nineteen : Prime 17 ∧ Prime 19 ∧ 19 = 17 + 2 := by native_decide
1178
1179/-- 29 and 31 are twin primes. -/
1180theorem twin_prime_twentynine_thirtyone : Prime 29 ∧ Prime 31 ∧ 31 = 29 + 2 := by native_decide
1181
1182/-- 41 and 43 are twin primes. -/
1183theorem twin_prime_fortyone_fortythree : Prime 41 ∧ Prime 43 ∧ 43 = 41 + 2 := by native_decide
1184
1185/-- 59 and 61 are twin primes. -/
1186theorem twin_prime_fiftynine_sixtyone : Prime 59 ∧ Prime 61 ∧ 61 = 59 + 2 := by native_decide
1187
1188/-- 71 and 73 are twin primes. -/
1189theorem twin_prime_seventyone_seventythree : Prime 71 ∧ Prime 73 ∧ 73 = 71 + 2 := by native_decide
1190
1191/-! ### More arithmetic function values at RS-related numbers -/
1192
1193/-- ω(120) = 3 (distinct prime factors: 2, 3, 5). -/
1194theorem omega_onehundredtwenty : omega 120 = 3 := by native_decide
1195
1196/-- Ω(120) = 5 (120 = 2³ × 3 × 5). -/
1197theorem bigOmega_onehundredtwenty : bigOmega 120 = 5 := by native_decide
1198
1199/-- σ_1(120) = 360. -/
1200theorem sigma_one_onehundredtwenty : sigma 1 120 = 360 := by native_decide
1201
1202/-- σ_0(120) = 16. -/
1203theorem sigma_zero_onehundredtwenty : sigma 0 120 = 16 := by native_decide
1204