`semiprime_sixtytwo`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 1774 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 1774.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

1771theorem semiprime_fiftyeight : isSemiprime 58 = true := by native_decide
1772
1773/-- 62 = 2 × 31 is semiprime. -/
1774theorem semiprime_sixtytwo : isSemiprime 62 = true := by native_decide
1775
1776/-- 65 = 5 × 13 is semiprime. -/
1777theorem semiprime_sixtyfive : isSemiprime 65 = true := by native_decide
1778
1779/-- 74 = 2 × 37 is semiprime (RS-relevant: 37). -/
1780theorem semiprime_seventyfour : isSemiprime 74 = true := by native_decide
1781
1782/-- 77 = 7 × 11 is semiprime. -/
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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.