theorem
proved
semiprime_eightyfive
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 1786.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
1783theorem semiprime_seventyseven : isSemiprime 77 = true := by native_decide
1784
1785/-- 85 = 5 × 17 is semiprime (RS-relevant: 17). -/
1786theorem semiprime_eightyfive : isSemiprime 85 = true := by native_decide
1787
1788/-- 91 = 7 × 13 is semiprime. -/
1789theorem semiprime_ninetyone : isSemiprime 91 = true := by native_decide
1790
1791/-- 95 = 5 × 19 is semiprime. -/
1792theorem semiprime_ninetyfive : isSemiprime 95 = true := by native_decide
1793
1794/-! ### Powers of 2 -/
1795
1796/-- 2^10 = 1024. -/
1797theorem two_pow_ten : (2 : ℕ) ^ 10 = 1024 := by native_decide
1798
1799/-- 2^12 = 4096. -/
1800theorem two_pow_twelve : (2 : ℕ) ^ 12 = 4096 := by native_decide
1801
1802/-- 2^16 = 65536. -/
1803theorem two_pow_sixteen : (2 : ℕ) ^ 16 = 65536 := by native_decide
1804
1805/-- 2^20 = 1048576. -/
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