`isPerfect_six`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 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). -/

papers checked against this theorem

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