The harmonic series diverges

src/analysis/convergent-series-metric-abelian-groups.lagda.md

@@ -43,7 +43,7 @@ module _
   is-sum-prop-series-Metric-Ab =
     is-limit-prop-sequence-Metric-Space
       ( metric-space-Metric-Ab G)
-      ( partial-sum-series-Metric-Ab G σ)
+      ( partial-sum-series-Metric-Ab σ)
 
   is-sum-series-Metric-Ab : type-Metric-Ab G → UU l2
   is-sum-series-Metric-Ab s = type-Prop (is-sum-prop-series-Metric-Ab s)
@@ -52,7 +52,7 @@ module _
   is-convergent-prop-series-Metric-Ab =
     subtype-convergent-sequence-Metric-Space
       ( metric-space-Metric-Ab G)
-      ( partial-sum-series-Metric-Ab G σ)
+      ( partial-sum-series-Metric-Ab σ)
 
   is-convergent-series-Metric-Ab : UU (l1 ⊔ l2)
   is-convergent-series-Metric-Ab =
@@ -76,7 +76,7 @@ module _
 
   partial-sum-convergent-series-Metric-Ab : sequence (type-Metric-Ab G)
   partial-sum-convergent-series-Metric-Ab =
-    partial-sum-series-Metric-Ab G series-convergent-series-Metric-Ab
+    partial-sum-series-Metric-Ab series-convergent-series-Metric-Ab
 ```
 
 ## The partial sums of a convergent series have a limit, the sum of the series

src/analysis/series-metric-abelian-groups.lagda.md

@@ -83,7 +83,7 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (G : Metric-Ab l1 l2)
+  {l1 l2 : Level} {G : Metric-Ab l1 l2}
   where
 
   partial-sum-series-Metric-Ab : series-Metric-Ab G → ℕ → type-Metric-Ab G
@@ -95,14 +95,14 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (G : Metric-Ab l1 l2)
+  {l1 l2 : Level} {G : Metric-Ab l1 l2}
   where
 
   eq-term-diff-partial-sum-series-Metric-Ab :
     (f : series-Metric-Ab G) (n : ℕ) →
     add-Metric-Ab G
-      ( partial-sum-series-Metric-Ab G f (succ-ℕ n))
-      ( neg-Metric-Ab G (partial-sum-series-Metric-Ab G f n)) ＝
+      ( partial-sum-series-Metric-Ab f (succ-ℕ n))
+      ( neg-Metric-Ab G (partial-sum-series-Metric-Ab f n)) ＝
     term-series-Metric-Ab f n
   eq-term-diff-partial-sum-series-Metric-Ab (series-terms-Metric-Ab f) n =
     ap-add-Metric-Ab G
@@ -118,21 +118,21 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (G : Metric-Ab l1 l2)
+  {l1 l2 : Level} {G : Metric-Ab l1 l2}
   where
 
   htpy-htpy-partial-sum-series-Metric-Ab :
     {σ τ : series-Metric-Ab G} →
-    (partial-sum-series-Metric-Ab G σ ~ partial-sum-series-Metric-Ab G τ) →
+    (partial-sum-series-Metric-Ab σ ~ partial-sum-series-Metric-Ab τ) →
     term-series-Metric-Ab σ ~ term-series-Metric-Ab τ
   htpy-htpy-partial-sum-series-Metric-Ab {σ} {τ} psσ~psτ n =
-    inv (eq-term-diff-partial-sum-series-Metric-Ab G σ n) ∙
+    inv (eq-term-diff-partial-sum-series-Metric-Ab σ n) ∙
     ap-right-subtraction-Ab (ab-Metric-Ab G) (psσ~psτ (succ-ℕ n)) (psσ~psτ n) ∙
-    eq-term-diff-partial-sum-series-Metric-Ab G τ n
+    eq-term-diff-partial-sum-series-Metric-Ab τ n
 
   eq-htpy-partial-sum-series-Metric-Ab :
     {σ τ : series-Metric-Ab G} →
-    (partial-sum-series-Metric-Ab G σ ~ partial-sum-series-Metric-Ab G τ) →
+    (partial-sum-series-Metric-Ab σ ~ partial-sum-series-Metric-Ab τ) →
     σ ＝ τ
   eq-htpy-partial-sum-series-Metric-Ab psσ~psτ =
     eq-htpy-term-series-Metric-Ab G
@@ -155,31 +155,30 @@ module _
 
 ```agda
 module _
-  {l1 l2 : Level} (G : Metric-Ab l1 l2)
+  {l1 l2 : Level} {G : Metric-Ab l1 l2}
   where
 
   abstract
     partial-sum-drop-series-Metric-Ab :
-      (n : ℕ) → (σ : series-Metric-Ab G) → (i : ℕ) →
-      partial-sum-series-Metric-Ab G (drop-series-Metric-Ab n σ) i ＝
+      (n : ℕ) (σ : series-Metric-Ab G) (i : ℕ) →
+      partial-sum-series-Metric-Ab (drop-series-Metric-Ab n σ) i ＝
       diff-Metric-Ab G
-        ( partial-sum-series-Metric-Ab G σ (n +ℕ i))
-        ( partial-sum-series-Metric-Ab G σ n)
-    partial-sum-drop-series-Metric-Ab n (series-terms-Metric-Ab σ) i =
+        ( partial-sum-series-Metric-Ab σ (n +ℕ i))
+        ( partial-sum-series-Metric-Ab σ n)
+    partial-sum-drop-series-Metric-Ab n s@(series-terms-Metric-Ab σ) i =
       inv
         ( equational-reasoning
           diff-Metric-Ab G
-            ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ)
-              ( n +ℕ i))
-            ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n)
+            ( partial-sum-series-Metric-Ab s (n +ℕ i))
+            ( partial-sum-series-Metric-Ab s n)
           ＝
             diff-Metric-Ab G
               ( add-Metric-Ab G
                 ( sum-fin-sequence-type-Ab (ab-Metric-Ab G) n
                   ( σ ∘ nat-Fin (n +ℕ i) ∘ inl-coproduct-Fin n i))
                 ( sum-fin-sequence-type-Ab (ab-Metric-Ab G) i
                   ( σ ∘ nat-Fin (n +ℕ i) ∘ inr-coproduct-Fin n i)))
-              ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n)
+              ( partial-sum-series-Metric-Ab s n)
             by
               ap-diff-Metric-Ab G
                 ( split-sum-fin-sequence-type-Ab
@@ -191,10 +190,11 @@ module _
           ＝
             diff-Metric-Ab G
               ( add-Metric-Ab G
-                ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n)
-                ( partial-sum-series-Metric-Ab G
-                  ( series-terms-Metric-Ab (σ ∘ add-ℕ n)) i))
-              ( partial-sum-series-Metric-Ab G (series-terms-Metric-Ab σ) n)
+                ( partial-sum-series-Metric-Ab s n)
+                ( partial-sum-series-Metric-Ab
+                  ( series-terms-Metric-Ab {G = G} (σ ∘ add-ℕ n))
+                  ( i)))
+              ( partial-sum-series-Metric-Ab s n)
             by
               ap-diff-Metric-Ab G
                 ( ap-add-Metric-Ab G
@@ -204,8 +204,8 @@ module _
                     ( λ j → ap σ (nat-inr-coproduct-Fin n i j))))
                 ( refl)
           ＝
-            partial-sum-series-Metric-Ab G
-              ( series-terms-Metric-Ab (σ ∘ add-ℕ n))
+            partial-sum-series-Metric-Ab
+              ( series-terms-Metric-Ab {G = G} (σ ∘ add-ℕ n))
               ( i)
             by is-identity-left-conjugation-Ab (ab-Metric-Ab G) _ _)
 ```

src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-rings.lagda.md

@@ -8,6 +8,7 @@ module commutative-algebra.sums-of-finite-sequences-of-elements-commutative-ring
 
 ```agda
 open import commutative-algebra.commutative-rings
+open import commutative-algebra.multiples-of-elements-commutative-rings
 
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -244,6 +245,19 @@ module _
     preserves-sum-permutation-fin-sequence-type-Ring (ring-Commutative-Ring A)
 ```
 
+### The sum of a constant finite sequence in a commutative ring is scalar multiplication by the length of the sequence
+
+```agda
+abstract
+  sum-constant-fin-sequence-type-Commutative-Ring :
+    {l : Level} (R : Commutative-Ring l) (n : ℕ) →
+    (x : type-Commutative-Ring R) →
+    sum-fin-sequence-type-Commutative-Ring R n (λ _ → x) ＝
+    multiple-Commutative-Ring R n x
+  sum-constant-fin-sequence-type-Commutative-Ring R =
+    sum-constant-fin-sequence-type-Ring (ring-Commutative-Ring R)
+```
+
 ## See also
 
 - [Sums of finite families of elements in commutative rings](commutative-algebra.sums-of-finite-families-of-elements-commutative-rings.md)

src/commutative-algebra/sums-of-finite-sequences-of-elements-commutative-semirings.lagda.md

@@ -8,6 +8,7 @@ module commutative-algebra.sums-of-finite-sequences-of-elements-commutative-semi
 
 ```agda
 open import commutative-algebra.commutative-semirings
+open import commutative-algebra.multiples-of-elements-commutative-semirings
 
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.natural-numbers
@@ -260,3 +261,16 @@ module _
     preserves-sum-permutation-fin-sequence-type-Semiring
       ( semiring-Commutative-Semiring R)
 ```
+
+### The sum of a constant finite sequence in a commutative semiring is scalar multiplication by the length of the sequence
+
+```agda
+abstract
+  sum-constant-fin-sequence-type-Commutative-Semiring :
+    {l : Level} (R : Commutative-Semiring l) (n : ℕ) →
+    (x : type-Commutative-Semiring R) →
+    sum-fin-sequence-type-Commutative-Semiring R n (λ _ → x) ＝
+    multiple-Commutative-Semiring R n x
+  sum-constant-fin-sequence-type-Commutative-Semiring R =
+    sum-constant-fin-sequence-type-Semiring (semiring-Commutative-Semiring R)
+```

src/elementary-number-theory.lagda.md

@@ -92,6 +92,7 @@ open import elementary-number-theory.greatest-common-divisor-natural-numbers pub
 open import elementary-number-theory.group-of-integers public
 open import elementary-number-theory.half-integers public
 open import elementary-number-theory.hardy-ramanujan-number public
+open import elementary-number-theory.harmonic-series-rational-numbers public
 open import elementary-number-theory.inclusion-natural-numbers-conatural-numbers public
 open import elementary-number-theory.inequalities-positive-and-negative-rational-numbers public
 open import elementary-number-theory.inequality-arithmetic-geometric-means-integers public
@@ -200,6 +201,7 @@ open import elementary-number-theory.ring-extension-rational-numbers-of-rational
 open import elementary-number-theory.ring-of-integers public
 open import elementary-number-theory.ring-of-rational-numbers public
 open import elementary-number-theory.semiring-of-natural-numbers public
+open import elementary-number-theory.series-rational-numbers public
 open import elementary-number-theory.sieve-of-eratosthenes public
 open import elementary-number-theory.square-free-natural-numbers public
 open import elementary-number-theory.square-roots-positive-rational-numbers public
@@ -219,6 +221,7 @@ open import elementary-number-theory.strict-inequality-rational-numbers public
 open import elementary-number-theory.strict-inequality-standard-finite-types public
 open import elementary-number-theory.strictly-ordered-pairs-of-natural-numbers public
 open import elementary-number-theory.strong-induction-natural-numbers public
+open import elementary-number-theory.sums-of-finite-sequences-of-rational-numbers public
 open import elementary-number-theory.sums-of-natural-numbers public
 open import elementary-number-theory.sylvesters-sequence public
 open import elementary-number-theory.taxicab-numbers public

src/elementary-number-theory/exponentiation-natural-numbers.lagda.md

@@ -12,10 +12,12 @@ open import commutative-algebra.powers-of-elements-commutative-semirings
 open import elementary-number-theory.addition-natural-numbers
 open import elementary-number-theory.multiplication-natural-numbers
 open import elementary-number-theory.natural-numbers
+open import elementary-number-theory.nonzero-natural-numbers
 open import elementary-number-theory.products-of-natural-numbers
 open import elementary-number-theory.semiring-of-natural-numbers
 
 open import foundation.action-on-identifications-functions
+open import foundation.dependent-pair-types
 open import foundation.identity-types
 ```
 
@@ -103,6 +105,9 @@ abstract
   is-nonzero-exp-ℕ m zero-ℕ p = is-nonzero-one-ℕ
   is-nonzero-exp-ℕ m (succ-ℕ n) p =
     is-nonzero-mul-ℕ (m ^ℕ n) m (is-nonzero-exp-ℕ m n p) p
+
+exp-ℕ⁺ : ℕ⁺ → ℕ → ℕ⁺
+exp-ℕ⁺ (n , n≠0) m = (exp-ℕ n m , is-nonzero-exp-ℕ n m n≠0)
 ```
 
 ### The exponent $m^n$ is equal to the $n$-fold product of $m$