`prime_threehundredfiftynine`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

2009theorem prime_threehundredfiftythree : Prime 353 := by native_decide
2010
2011/-- 359 is prime. -/
2012theorem prime_threehundredfiftynine : Prime 359 := by native_decide
2013
2014/-- 367 is prime. -/
2015theorem prime_threehundredsixtyseven : Prime 367 := by native_decide
2016
2017/-- 373 is prime. -/
2018theorem prime_threehundredseventythree : Prime 373 := by native_decide
2019
2020/-- 379 is prime. -/
2021theorem prime_threehundredseventynine : Prime 379 := by native_decide
2022
2023/-- 383 is prime. -/
2024theorem prime_threehundredeightythree : Prime 383 := by native_decide
2025
2026/-- 389 is prime. -/
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

papers checked against this theorem

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