theorem
proved
two_pow_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 1815.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
1812theorem two_pow_five : (2 : ℕ) ^ 5 = 32 := by native_decide
1813
1814/-- 2^6 = 64. -/
1815theorem two_pow_six : (2 : ℕ) ^ 6 = 64 := by native_decide
1816
1817/-- 2^7 = 128. -/
1818theorem two_pow_seven : (2 : ℕ) ^ 7 = 128 := by native_decide
1819
1820/-- 2^8 = 256. -/
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