`isPerfect`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 609 · 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 609.

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

used by

formal source

 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
 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

papers checked against this theorem

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