def
definition
isFourAlmostPrime
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2219.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
four_almost_prime_eightyeight -
four_almost_prime_eightyfour -
four_almost_prime_eightyone -
four_almost_prime_fiftyfour -
four_almost_prime_fiftysix -
four_almost_prime_forty -
four_almost_prime_ninety -
four_almost_prime_onehundred -
four_almost_prime_onehundredforty -
four_almost_prime_onehundredfour -
four_almost_prime_onehundredthirtysix -
four_almost_prime_onehundredthirtytwo -
four_almost_prime_onehundredtwentysix -
four_almost_prime_sixteen -
four_almost_prime_sixty -
four_almost_prime_thirtysix -
four_almost_prime_twentyfour
formal source
2216/-! ### 4-almost primes (Ω(n) = 4) -/
2217
2218/-- A number is 4-almost prime if Ω(n) = 4. -/
2219def isFourAlmostPrime (n : ℕ) : Bool := bigOmega n = 4
2220
2221/-- 16 = 2⁴ is 4-almost prime. -/
2222theorem four_almost_prime_sixteen : isFourAlmostPrime 16 = true := by native_decide
2223
2224/-- 24 = 2³ × 3 is 4-almost prime. -/
2225theorem four_almost_prime_twentyfour : isFourAlmostPrime 24 = true := by native_decide
2226
2227/-- 36 = 2² × 3² is 4-almost prime. -/
2228theorem four_almost_prime_thirtysix : isFourAlmostPrime 36 = true := by native_decide
2229
2230/-- 40 = 2³ × 5 is 4-almost prime. -/
2231theorem four_almost_prime_forty : isFourAlmostPrime 40 = true := by native_decide
2232
2233/-- 54 = 2 × 3³ is 4-almost prime. -/
2234theorem four_almost_prime_fiftyfour : isFourAlmostPrime 54 = true := by native_decide
2235
2236/-- 56 = 2³ × 7 is 4-almost prime. -/
2237theorem four_almost_prime_fiftysix : isFourAlmostPrime 56 = true := by native_decide
2238
2239/-- 60 = 2² × 3 × 5 is 4-almost prime. -/
2240theorem four_almost_prime_sixty : isFourAlmostPrime 60 = true := by native_decide
2241
2242/-- 81 = 3⁴ is 4-almost prime. -/
2243theorem four_almost_prime_eightyone : isFourAlmostPrime 81 = true := by native_decide
2244
2245/-- 84 = 2² × 3 × 7 is 4-almost prime. -/
2246theorem four_almost_prime_eightyfour : isFourAlmostPrime 84 = true := by native_decide
2247
2248/-- 88 = 2³ × 11 is 4-almost prime (RS-relevant: 11). -/
2249theorem four_almost_prime_eightyeight : isFourAlmostPrime 88 = true := by native_decide