`six_almost_prime_sixtyfour`

proved

show as: view math explainer →

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

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

2677def isSixAlmostPrime (n : ℕ) : Bool := bigOmega n = 6
2678
2679/-- 64 = 2⁶ is 6-almost prime. -/
2680theorem six_almost_prime_sixtyfour : isSixAlmostPrime 64 = true := by native_decide
2681
2682/-- 96 = 2⁵ × 3 is 6-almost prime. -/
2683theorem six_almost_prime_ninetysix : isSixAlmostPrime 96 = true := by native_decide
2684
2685/-- 144 = 2⁴ × 3² is 6-almost prime. -/
2686theorem six_almost_prime_onehundredfortyfour : isSixAlmostPrime 144 = true := by native_decide
2687
2688/-- 160 = 2⁵ × 5 is 6-almost prime. -/
2689theorem six_almost_prime_onehundredsixty : isSixAlmostPrime 160 = true := by native_decide
2690
2691/-- 216 = 2³ × 3³ is 6-almost prime. -/
2692theorem six_almost_prime_twohundredsixteen : isSixAlmostPrime 216 = true := by native_decide
2693
2694/-- 224 = 2⁵ × 7 is 6-almost prime. -/
2695theorem six_almost_prime_twohundredtwentyfour : isSixAlmostPrime 224 = true := by native_decide
2696
2697/-- 240 = 2⁴ × 3 × 5 is 6-almost prime (RS-relevant). -/
2698theorem six_almost_prime_twohundredforty : isSixAlmostPrime 240 = true := by native_decide
2699
2700-- Note: 288 = 2⁵ × 3², Ω = 5 + 2 = 7, so not 6-almost prime.
2701
2702/-- 324 = 2² × 3⁴ is 6-almost prime. -/
2703theorem six_almost_prime_threehundredtwentyfour : isSixAlmostPrime 324 = true := by native_decide
2704
2705/-- 352 = 2⁵ × 11 is 6-almost prime (RS-relevant: 11). -/
2706theorem six_almost_prime_threehundredfiftytwo : isSixAlmostPrime 352 = true := by native_decide
2707
2708/-- 360 = 2³ × 3² × 5 is 6-almost prime (RS-relevant: main superperiod). -/
2709theorem six_almost_prime_threehundredsixty : isSixAlmostPrime 360 = true := by native_decide
2710

papers checked against this theorem

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