`five_almost_prime_seventytwo`

proved

show as: view math explainer →

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

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

2440theorem five_almost_prime_fortyeight : isFiveAlmostPrime 48 = true := by native_decide
2441
2442/-- 72 = 2³ × 3² is 5-almost prime. -/
2443theorem five_almost_prime_seventytwo : isFiveAlmostPrime 72 = true := by native_decide
2444
2445/-- 80 = 2⁴ × 5 is 5-almost prime. -/
2446theorem five_almost_prime_eighty : isFiveAlmostPrime 80 = true := by native_decide
2447
2448/-- 108 = 2² × 3³ is 5-almost prime. -/
2449theorem five_almost_prime_onehundredeight : isFiveAlmostPrime 108 = true := by native_decide
2450
2451/-- 112 = 2⁴ × 7 is 5-almost prime. -/
2452theorem five_almost_prime_onehundredtwelve : isFiveAlmostPrime 112 = true := by native_decide
2453
2454/-- 120 = 2³ × 3 × 5 is 5-almost prime (RS-relevant). -/
2455theorem five_almost_prime_onehundredtwenty : isFiveAlmostPrime 120 = true := by native_decide
2456
2457/-- 162 = 2 × 3⁴ is 5-almost prime. -/
2458theorem five_almost_prime_onehundredsixtytwo : isFiveAlmostPrime 162 = true := by native_decide
2459
2460/-- 176 = 2⁴ × 11 is 5-almost prime (RS-relevant: 11). -/
2461theorem five_almost_prime_onehundredseventysix : isFiveAlmostPrime 176 = true := by native_decide
2462
2463/-- 180 = 2² × 3² × 5 is 5-almost prime. -/
2464theorem five_almost_prime_onehundredeighty : isFiveAlmostPrime 180 = true := by native_decide
2465
2466/-- 200 = 2³ × 5² is 5-almost prime. -/
2467theorem five_almost_prime_twohundred : isFiveAlmostPrime 200 = true := by native_decide
2468
2469/-- 208 = 2⁴ × 13 is 5-almost prime. -/
2470theorem five_almost_prime_twohundredeight : isFiveAlmostPrime 208 = true := by native_decide
2471
2472-- Note: 240 = 2⁴ × 3 × 5, Ω = 4 + 1 + 1 = 6, so 240 is 6-almost prime, not 5-almost prime
2473

papers checked against this theorem

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