theorem
proved
prime_threehundredninetyseven
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 2030.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
2027theorem prime_threehundredeightynine : Prime 389 := by native_decide
2028
2029/-- 397 is prime. -/
2030theorem prime_threehundredninetyseven : Prime 397 := by native_decide
2031
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