theorem
proved
liouville_twohundredten
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1343.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1340theorem radical_twohundredten : radical 210 = 210 := by native_decide
1341
1342/-- λ(210) = 1 (Liouville, Ω = 4 is even). -/
1343theorem liouville_twohundredten : liouville 210 = 1 := by native_decide
1344
1345-- Note: μ(210) = 1 already exists as mobius_twohundredten
1346
1347/-! ### Additional small primes -/
1348
1349/-- 19 is prime. -/
1350theorem prime_nineteen : Prime 19 := by native_decide
1351
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