def
definition
isThreeAlmostPrime
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 2035.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
-
three_almost_prime_eight -
three_almost_prime_eighteen -
three_almost_prime_fifty -
three_almost_prime_fiftytwo -
three_almost_prime_fortyfive -
three_almost_prime_fortyfour -
three_almost_prime_fortytwo -
three_almost_prime_seventy -
three_almost_prime_seventyfive -
three_almost_prime_seventysix -
three_almost_prime_sixtyeight -
three_almost_prime_sixtysix -
three_almost_prime_sixtythree -
three_almost_prime_thirty -
three_almost_prime_twelve -
three_almost_prime_twenty -
three_almost_prime_twentyeight -
three_almost_prime_twentyseven
formal source
2032/-! ### 3-almost primes (Ω(n) = 3) -/
2033
2034/-- A number is 3-almost prime if Ω(n) = 3. -/
2035def isThreeAlmostPrime (n : ℕ) : Bool := bigOmega n = 3
2036
2037/-- 8 = 2³ is 3-almost prime. -/
2038theorem three_almost_prime_eight : isThreeAlmostPrime 8 = true := by native_decide
2039
2040/-- 12 = 2² × 3 is 3-almost prime. -/
2041theorem three_almost_prime_twelve : isThreeAlmostPrime 12 = true := by native_decide
2042
2043/-- 18 = 2 × 3² is 3-almost prime. -/
2044theorem three_almost_prime_eighteen : isThreeAlmostPrime 18 = true := by native_decide
2045
2046/-- 20 = 2² × 5 is 3-almost prime. -/
2047theorem three_almost_prime_twenty : isThreeAlmostPrime 20 = true := by native_decide
2048
2049/-- 27 = 3³ is 3-almost prime. -/
2050theorem three_almost_prime_twentyseven : isThreeAlmostPrime 27 = true := by native_decide
2051
2052/-- 28 = 2² × 7 is 3-almost prime. -/
2053theorem three_almost_prime_twentyeight : isThreeAlmostPrime 28 = true := by native_decide
2054
2055/-- 30 = 2 × 3 × 5 is 3-almost prime. -/
2056theorem three_almost_prime_thirty : isThreeAlmostPrime 30 = true := by native_decide
2057
2058/-- 42 = 2 × 3 × 7 is 3-almost prime. -/
2059theorem three_almost_prime_fortytwo : isThreeAlmostPrime 42 = true := by native_decide
2060
2061/-- 44 = 2² × 11 is 3-almost prime. -/
2062theorem three_almost_prime_fortyfour : isThreeAlmostPrime 44 = true := by native_decide
2063
2064/-- 45 = 3² × 5 is 3-almost prime (RS constant). -/
2065theorem three_almost_prime_fortyfive : isThreeAlmostPrime 45 = true := by native_decide