theorem
proved
practical_eighteen
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 2143.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2140theorem practical_sixteen : sigma 1 16 ≥ 16 := by native_decide
2141
2142/-- σ_1(18) = 39 ≥ 18, so 18 is practical. -/
2143theorem practical_eighteen : sigma 1 18 ≥ 18 := by native_decide
2144
2145/-- σ_1(20) = 42 ≥ 20, so 20 is practical. -/
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