`semiprime_fifteen`

proved

show as: view math explainer →

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

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

1726theorem semiprime_fourteen : isSemiprime 14 = true := by native_decide
1727
1728/-- 15 = 3 × 5 is semiprime. -/
1729theorem semiprime_fifteen : isSemiprime 15 = true := by native_decide
1730
1731/-- 21 = 3 × 7 is semiprime. -/
1732theorem semiprime_twentyone : isSemiprime 21 = true := by native_decide
1733
1734/-- 22 = 2 × 11 is semiprime. -/
1735theorem semiprime_twentytwo : isSemiprime 22 = true := by native_decide
1736
1737/-- 25 = 5² is semiprime. -/
1738theorem semiprime_twentyfive : isSemiprime 25 = true := by native_decide
1739
1740/-- 26 = 2 × 13 is semiprime. -/
1741theorem semiprime_twentysix : isSemiprime 26 = true := by native_decide
1742
1743/-- 33 = 3 × 11 is semiprime. -/
1744theorem semiprime_thirtythree : isSemiprime 33 = true := by native_decide
1745
1746/-- 34 = 2 × 17 is semiprime. -/
1747theorem semiprime_thirtyfour : isSemiprime 34 = true := by native_decide
1748
1749/-- 35 = 5 × 7 is semiprime. -/
1750theorem semiprime_thirtyfive : isSemiprime 35 = true := by native_decide
1751
1752/-- 38 = 2 × 19 is semiprime. -/
1753theorem semiprime_thirtyeight : isSemiprime 38 = true := by native_decide
1754
1755/-- 39 = 3 × 13 is semiprime. -/
1756theorem semiprime_thirtynine : isSemiprime 39 = true := by native_decide
1757
1758/-- 49 = 7² is semiprime. -/
1759theorem semiprime_fortynine : isSemiprime 49 = true := by native_decide

papers checked against this theorem

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