theorem
proved
practical_one
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2122.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2119/-! ### Practical numbers (every m ≤ n is a sum of distinct divisors of n) -/
2120
2121/-- σ_1(1) = 1 ≥ 1, so 1 is practical. -/
2122theorem practical_one : sigma 1 1 ≥ 1 := by native_decide
2123
2124/-- σ_1(2) = 3 ≥ 2, so 2 is practical. -/
2125theorem practical_two : sigma 1 2 ≥ 2 := by native_decide
2126
2127/-- σ_1(4) = 7 ≥ 4, so 4 is practical. -/
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