`semiprime_fortynine`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 1759 · 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 1759.

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

1756theorem semiprime_thirtynine : isSemiprime 39 = true := by native_decide
1757
1758/-- 49 = 7² is semiprime. -/
1759theorem semiprime_fortynine : isSemiprime 49 = true := by native_decide
1760
1761/-- 51 = 3 × 17 is semiprime. -/
1762theorem semiprime_fiftyone : isSemiprime 51 = true := by native_decide
1763
1764/-- 55 = 5 × 11 is semiprime. -/
1765theorem semiprime_fiftyfive : isSemiprime 55 = true := by native_decide
1766
1767/-- 57 = 3 × 19 is semiprime. -/
1768theorem semiprime_fiftyseven : isSemiprime 57 = true := by native_decide
1769
1770/-- 58 = 2 × 29 is semiprime. -/
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

papers checked against this theorem

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