`prime_onehundredthirtynine`

proved

show as: view math explainer →

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

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

Prime IndisputableMonolith.NumberTheory.Primes.Basic

formal source

 957theorem prime_onehundredthirteen : Prime 113 := by native_decide
 958theorem prime_onehundredtwentyseven : Prime 127 := by native_decide
 959theorem prime_onehundredthirtyone : Prime 131 := by native_decide
 960theorem prime_onehundredthirtynine : Prime 139 := by native_decide
 961theorem prime_onehundredfortynine : Prime 149 := by native_decide
 962theorem prime_onehundredfiftyone : Prime 151 := by native_decide
 963theorem prime_onehundredfiftyseven : Prime 157 := by native_decide
 964theorem prime_onehundredsixtythree : Prime 163 := by native_decide
 965theorem prime_onehundredsixtyseven : Prime 167 := by native_decide
 966theorem prime_onehundredseventythree : Prime 173 := by native_decide
 967theorem prime_onehundredseventynine : Prime 179 := by native_decide
 968theorem prime_onehundredeightyone : Prime 181 := by native_decide
 969theorem prime_onehundredninetyone : Prime 191 := by native_decide
 970theorem prime_onehundredninetythree : Prime 193 := by native_decide
 971theorem prime_onehundredninetyseven : Prime 197 := by native_decide
 972theorem prime_onehundredninetynine : Prime 199 := by native_decide
 973
 974/-! ### Sigma values at small composites -/
 975
 976/-- σ_0(6) = 4 (divisors: 1, 2, 3, 6). -/
 977theorem sigma_zero_six : sigma 0 6 = 4 := by native_decide
 978
 979/-- σ_1(6) = 12 (sum: 1 + 2 + 3 + 6 = 12). -/
 980theorem sigma_one_six : sigma 1 6 = 12 := by native_decide
 981
 982/-- σ_0(10) = 4 (divisors: 1, 2, 5, 10). -/
 983theorem sigma_zero_ten : sigma 0 10 = 4 := by native_decide
 984
 985/-- σ_1(10) = 18 (sum: 1 + 2 + 5 + 10 = 18). -/
 986theorem sigma_one_ten : sigma 1 10 = 18 := by native_decide
 987
 988/-- σ_0(12) = 6 (divisors: 1, 2, 3, 4, 6, 12). -/
 989theorem sigma_zero_twelve : sigma 0 12 = 6 := by native_decide
 990

papers checked against this theorem

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