--- a/src/HOL/Analysis/Infinite_Sum.thy Tue Jan 17 15:55:52 2023 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy Tue Jan 17 16:08:54 2023 +0100
@@ -9,13 +9,6 @@
section \<open>Infinite sums\<close>
\<^latex>\<open>\label{section:Infinite_Sum}\<close>
-theory Infinite_Sum
- imports
- Elementary_Topology
- "HOL-Library.Extended_Nonnegative_Real"
- "HOL-Library.Complex_Order"
-begin
-
text \<open>In this theory, we introduce the definition of infinite sums, i.e., sums ranging over an
infinite, potentially uncountable index set with no particular ordering.
(This is different from series. Those are sums indexed by natural numbers,
@@ -29,6 +22,12 @@
commutative monoid endowed with a Hausdorff topology.
(Examples are reals, complex numbers, normed vector spaces, and more.)\<close>
+theory Infinite_Sum
+ imports
+ Elementary_Topology
+ "HOL-Library.Extended_Nonnegative_Real"
+ "HOL-Library.Complex_Order"
+begin
subsection \<open>Definition and syntax\<close>