theorem
proved
primeCounting_twohundred
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 631.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
628theorem primeCounting_fifty : primeCounting 50 = 15 := by native_decide
629
630/-- π(200) = 46. -/
631theorem primeCounting_twohundred : primeCounting 200 = 46 := by native_decide
632
633/-- π(1000) = 168. -/
634theorem primeCounting_thousand : primeCounting 1000 = 168 := by native_decide
635
636/-! ### Ω and ω for RS constants -/
637
638/-- Ω(8) = 3 (since 8 = 2³). -/
639theorem bigOmega_eight : bigOmega 8 = 3 := by native_decide
640
641/-- Ω(45) = 3 (since 45 = 3² × 5). -/
642theorem bigOmega_fortyfive : bigOmega 45 = 3 := by native_decide
643
644/-- Ω(360) = 6 (since 360 = 2³ × 3² × 5). -/
645theorem bigOmega_threehundredsixty : bigOmega 360 = 6 := by native_decide
646
647/-- Ω(840) = 6 (since 840 = 2³ × 3 × 5 × 7, with 3+1+1+1 = 6 factors). -/
648theorem bigOmega_eighthundredforty : bigOmega 840 = 6 := by native_decide
649
650/-- ω(8) = 1 (only prime factor is 2). -/
651theorem omega_eight : omega 8 = 1 := by native_decide
652
653/-- ω(45) = 2 (prime factors are 3 and 5). -/
654theorem omega_fortyfive : omega 45 = 2 := by native_decide
655
656/-- ω(360) = 3 (prime factors are 2, 3, 5). -/
657theorem omega_threehundredsixty : omega 360 = 3 := by native_decide
658
659/-- ω(840) = 4 (prime factors are 2, 3, 5, 7). -/
660theorem omega_eighthundredforty : omega 840 = 4 := by native_decide
661