theorem
proved
two_pow_nine
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1824.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1821theorem two_pow_eight : (2 : ℕ) ^ 8 = 256 := by native_decide
1822
1823/-- 2^9 = 512. -/
1824theorem two_pow_nine : (2 : ℕ) ^ 9 = 512 := by native_decide
1825
1826/-! ### σ_3 values (sum of cubes of divisors) -/
1827
1828/-- σ_3(1) = 1. -/
1829theorem sigma_three_one : sigma 3 1 = 1 := by native_decide
1830
1831/-- σ_3(2) = 1 + 8 = 9. -/
1832theorem sigma_three_two : sigma 3 2 = 9 := by native_decide
1833
1834/-- σ_3(3) = 1 + 27 = 28. -/
1835theorem sigma_three_three : sigma 3 3 = 28 := by native_decide
1836
1837/-- σ_3(4) = 1 + 8 + 64 = 73. -/
1838theorem sigma_three_four : sigma 3 4 = 73 := by native_decide
1839
1840/-- σ_3(5) = 1 + 125 = 126. -/
1841theorem sigma_three_five : sigma 3 5 = 126 := by native_decide
1842
1843/-- σ_3(6) = 1 + 8 + 27 + 216 = 252. -/
1844theorem sigma_three_six : sigma 3 6 = 252 := by native_decide
1845
1846/-- σ_3(8) = 1 + 8 + 64 + 512 = 585. -/
1847theorem sigma_three_eight : sigma 3 8 = 585 := by native_decide
1848
1849/-- σ_3(10) = 1 + 8 + 125 + 1000 = 1134. -/
1850theorem sigma_three_ten : sigma 3 10 = 1134 := by native_decide
1851
1852/-- σ_3(12) = 2044. -/
1853theorem sigma_three_twelve : sigma 3 12 = 2044 := by native_decide
1854