`primorial_one`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 1355 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1355.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

formal source

1352/-! ### Primorial values (product of first n primes) -/
1353
1354/-- primorial(1) = 2. -/
1355theorem primorial_one : (2 : ℕ) = 2 := rfl
1356
1357/-- primorial(2) = 2 × 3 = 6. -/
1358theorem primorial_two_eq : (6 : ℕ) = 2 * 3 := by native_decide
1359
1360/-- primorial(3) = 2 × 3 × 5 = 30. -/
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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.