`five_almost_prime_thirtytwo`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

2434def isFiveAlmostPrime (n : ℕ) : Bool := bigOmega n = 5
2435
2436/-- 32 = 2⁵ is 5-almost prime. -/
2437theorem five_almost_prime_thirtytwo : isFiveAlmostPrime 32 = true := by native_decide
2438
2439/-- 48 = 2⁴ × 3 is 5-almost prime. -/
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

papers checked against this theorem

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