theorem
proved
sigma_zero_ten
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 983.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
991/-- σ_1(12) = 28 (sum: 1 + 2 + 3 + 4 + 6 + 12 = 28). -/
992theorem sigma_one_twelve : sigma 1 12 = 28 := by native_decide
993
994/-- σ_0(30) = 8. -/
995theorem sigma_zero_thirty : sigma 0 30 = 8 := by native_decide
996
997/-- σ_1(30) = 72. -/
998theorem sigma_one_thirty : sigma 1 30 = 72 := by native_decide
999
1000/-! ### Totient at small composites -/
1001
1002/-- φ(10) = 4. -/
1003theorem totient_ten : totient 10 = 4 := by native_decide
1004
1005/-- φ(12) = 4. -/
1006theorem totient_twelve : totient 12 = 4 := by native_decide
1007
1008/-- φ(30) = 8. -/
1009theorem totient_thirty : totient 30 = 8 := by native_decide
1010
1011/-- φ(24) = 8. -/
1012theorem totient_twentyfour : totient 24 = 8 := by native_decide
1013