theorem
proved
practical_twentyfour
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 2149.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2146theorem practical_twenty : sigma 1 20 ≥ 20 := by native_decide
2147
2148/-- σ_1(24) = 60 ≥ 24, so 24 is practical. -/
2149theorem practical_twentyfour : sigma 1 24 ≥ 24 := by native_decide
2150
2151/-- σ_1(28) = 56 ≥ 28, so 28 is practical. -/
2152theorem practical_twentyeight : sigma 1 28 ≥ 28 := by native_decide
2153
2154/-- σ_1(30) = 72 ≥ 30, so 30 is practical. -/
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