theorem
proved
practical_six
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 2131.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2128theorem practical_four : sigma 1 4 ≥ 4 := by native_decide
2129
2130/-- σ_1(6) = 12 ≥ 6, so 6 is practical. -/
2131theorem practical_six : sigma 1 6 ≥ 6 := by native_decide
2132
2133/-- σ_1(8) = 15 ≥ 8, so 8 is practical. -/
2134theorem practical_eight : sigma 1 8 ≥ 8 := by native_decide
2135
2136/-- σ_1(12) = 28 ≥ 12, so 12 is practical. -/
2137theorem practical_twelve : sigma 1 12 ≥ 12 := by native_decide
2138
2139/-- σ_1(16) = 31 ≥ 16, so 16 is practical. -/
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