theorem
proved
two_pow_four
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 1809.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
1806theorem two_pow_twenty : (2 : ℕ) ^ 20 = 1048576 := by native_decide
1807
1808/-- 2^4 = 16. -/
1809theorem two_pow_four : (2 : ℕ) ^ 4 = 16 := by native_decide
1810
1811/-- 2^5 = 32. -/
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