theorem
proved
bigOmega_factorial_three
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 601.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
598- 5! = 120 = 2³*3*5 → Ω = 5
599-/
600theorem bigOmega_factorial_two : bigOmega (Nat.factorial 2) = 1 := by native_decide
601theorem bigOmega_factorial_three : bigOmega (Nat.factorial 3) = 2 := by native_decide
602theorem bigOmega_factorial_four : bigOmega (Nat.factorial 4) = 4 := by native_decide
603theorem bigOmega_factorial_five : bigOmega (Nat.factorial 5) = 5 := by native_decide
604
605/-! ### Perfect numbers -/
606
607/-- A number n is perfect if σ_1(n) = 2n.
608We make this decidable for concrete values. -/
609def isPerfect (n : ℕ) : Prop := sigma 1 n = 2 * n
610
611instance : DecidablePred isPerfect := fun n => inferInstanceAs (Decidable (sigma 1 n = 2 * n))
612
613/-- 6 is perfect. -/
614theorem isPerfect_six : isPerfect 6 := by native_decide
615
616/-- 28 is perfect. -/
617theorem isPerfect_twentyeight : isPerfect 28 := by native_decide
618
619/-- 496 is perfect. -/
620theorem isPerfect_fourhundredninetysix : isPerfect 496 := by native_decide
621
622/-! ### More primeCounting values -/
623
624/-- π(30) = 10. -/
625theorem primeCounting_thirty : primeCounting 30 = 10 := by native_decide
626
627/-- π(50) = 15. -/
628theorem primeCounting_fifty : primeCounting 50 = 15 := by native_decide
629
630/-- π(200) = 46. -/
631theorem primeCounting_twohundred : primeCounting 200 = 46 := by native_decide