theorem
proved
practical_thirtytwo
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 2158.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2155theorem practical_thirty : sigma 1 30 ≥ 30 := by native_decide
2156
2157/-- σ_1(32) = 63 ≥ 32, so 32 is practical. -/
2158theorem practical_thirtytwo : sigma 1 32 ≥ 32 := by native_decide
2159
2160/-- σ_1(36) = 91 ≥ 36, so 36 is practical. -/
2161theorem practical_thirtysix : sigma 1 36 ≥ 36 := by native_decide
2162
2163/-! ### Primes in the 400s -/
2164
2165/-- 401 is prime. -/
2166theorem prime_fourhundredone : Prime 401 := by native_decide
2167
2168/-- 409 is prime. -/
2169theorem prime_fourhundrednine : Prime 409 := by native_decide
2170
2171/-- 419 is prime. -/
2172theorem prime_fourhundrednineteen : Prime 419 := by native_decide
2173
2174/-- 421 is prime. -/
2175theorem prime_fourhundredtwentyone : Prime 421 := by native_decide
2176
2177/-- 431 is prime. -/
2178theorem prime_fourhundredthirtyone : Prime 431 := by native_decide
2179
2180/-- 433 is prime. -/
2181theorem prime_fourhundredthirtythree : Prime 433 := by native_decide
2182
2183/-- 439 is prime. -/
2184theorem prime_fourhundredthirtynine : Prime 439 := by native_decide
2185
2186/-- 443 is prime. -/
2187theorem prime_fourhundredfortythree : Prime 443 := by native_decide
2188