theorem
proved
mobius_twothousandthreehundredten
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 1384.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
1395/-- 60 is highly composite (has more divisors than any smaller positive integer). -/
1396theorem divisors_card_sixty_gt : ∀ n, 0 < n → n < 60 → (n : ℕ).divisors.card < (60 : ℕ).divisors.card := by
1397 intro n hn hlt
1398 interval_cases n <;> native_decide
1399
1400/-- 120 is highly composite (has more divisors than any smaller positive integer). -/
1401theorem divisors_card_onehundredtwenty_gt : ∀ n, 0 < n → n < 120 → (n : ℕ).divisors.card < (120 : ℕ).divisors.card := by
1402 intro n hn hlt
1403 interval_cases n <;> native_decide
1404
1405/-! ### Safe primes (p such that (p-1)/2 is also prime) -/
1406
1407/-- 5 is a safe prime: (5-1)/2 = 2 is prime. -/
1408theorem safe_prime_five : Prime 5 ∧ Prime ((5 - 1) / 2) := by native_decide
1409
1410/-- 7 is a safe prime: (7-1)/2 = 3 is prime. -/
1411theorem safe_prime_seven : Prime 7 ∧ Prime ((7 - 1) / 2) := by native_decide
1412
1413/-- 11 is a safe prime: (11-1)/2 = 5 is prime. -/
1414theorem safe_prime_eleven : Prime 11 ∧ Prime ((11 - 1) / 2) := by native_decide