def
definition
isFiveAlmostPrime
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2434.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
five_almost_prime_eighty -
five_almost_prime_fortyeight -
five_almost_prime_onehundredeight -
five_almost_prime_onehundredeighty -
five_almost_prime_onehundredseventysix -
five_almost_prime_onehundredsixtytwo -
five_almost_prime_onehundredtwelve -
five_almost_prime_onehundredtwenty -
five_almost_prime_seventytwo -
five_almost_prime_thirtytwo -
five_almost_prime_twohundred -
five_almost_prime_twohundredeight -
five_almost_prime_twohundredfortythree -
five_almost_prime_twohundredseventytwo
formal source
2431/-! ### 5-almost primes (Ω(n) = 5) -/
2432
2433/-- A number is 5-almost prime if Ω(n) = 5. -/
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