theorem
proved
primorial_four_eq
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1364.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
1361theorem primorial_three_eq : (30 : ℕ) = 2 * 3 * 5 := by native_decide
1362
1363/-- primorial(4) = 2 × 3 × 5 × 7 = 210. -/
1364theorem primorial_four_eq : (210 : ℕ) = 2 * 3 * 5 * 7 := by native_decide
1365
1366/-- primorial(5) = 2 × 3 × 5 × 7 × 11 = 2310. -/
1367theorem primorial_five_eq : (2310 : ℕ) = 2 * 3 * 5 * 7 * 11 := by native_decide
1368
1369/-! ### More 2310-related (primorial(5)) -/
1370
1371/-- φ(2310) = 480. -/
1372theorem totient_twothousandthreehundredten : totient 2310 = 480 := by native_decide
1373
1374/-- ω(2310) = 5 (distinct prime factors: 2, 3, 5, 7, 11). -/
1375theorem omega_twothousandthreehundredten : omega 2310 = 5 := by native_decide
1376
1377/-- Ω(2310) = 5. -/
1378theorem bigOmega_twothousandthreehundredten : bigOmega 2310 = 5 := by native_decide
1379
1380/-- 2310 is squarefree. -/
1381theorem squarefree_twothousandthreehundredten : Squarefree 2310 := by native_decide
1382
1383/-- μ(2310) = -1 (squarefree with 5 prime factors). -/
1384theorem mobius_twothousandthreehundredten : mobius 2310 = -1 := by native_decide
1385
1386/-! ### Highly composite numbers -/
1387
1388/-- 12 is highly composite (has more divisors than any smaller positive integer). -/
1389theorem divisors_card_twelve_gt : ∀ n, 0 < n → n < 12 → (n : ℕ).divisors.card < (12 : ℕ).divisors.card := by
1390 intro n hn hlt
1391 interval_cases n <;> native_decide
1392
1393/-! ### More highly composite numbers -/
1394