avewright/proofwiki-math huggingface dataset:
Theorem: Existence of Abscissa of Absolute Convergence

Let $\ds \map f s = \sum_{n \mathop = 1}^\infty a_n n^{-s}$ be a Dirichlet series.
Let the series $\ds \sum_{n \mathop = 1}^\infty \size { a_n n^{-s} }$ not converge for all $s \in \C$, or diverge for all $s \in \C$.
Then there exists a real number $\sigma_a$ such that $\map f s$ converges absolutely for all $s = \sigma + it$ with $\sigma > \sigma_a$, and does not converge absolutely for all $s$ with $\sigma < \sigma_a$.
We call $\sigma_a$ the '''abscissa of absolute convergence''' of the Dirichlet series.

Proof:
Let $S$ be the set of all complex numbers $s$ such that $\map f s$ converges absolutely.
By hypothesis, there is some $s_0 = \sigma_0 + it_0 \in \C$ such that $\map f {s_0}$ converges absolutely, so $S$ is not empty.
Moreover, $S$ is bounded below, for otherwise it follows from Dirichlet Series Absolute Convergence Lemma that $\map f s$ converges absolutely for all $s \in \C$, a contradiction of our assumptions.
Therefore the infimum:
:$\sigma_a = \inf \set {\sigma: s = \sigma + i t \in S} \in \R$
is well defined.
Now if $s = \sigma + it$ with $\sigma > \sigma_a$, then there is $s' = \sigma' + i t' \in S$ with $\sigma' < \sigma$, and $\map f {s'}$ is absolutely convergent.
Then it follows from Dirichlet Series Absolute Convergence Lemma that $\map f s$ is absolutely convergent.
If $s = \sigma + it$ with $\sigma < \sigma_a$, and $\map f s$ is absolutely convergent then $s$ contradicts the definition of $\sigma_a$.
Therefore, $\sigma_a$ has the claimed properties.
{{qed}}
Theorem: Dirichlet Series Convergence Lemma

Let $\ds \map f s = \sum_{n \mathop = 1}^\infty \frac {a_n} {n^s}$ be a Dirichlet series.
Let $\map f s$ converge at $s_0 = \sigma_0 + i t_0$.
Then $\map f s$ converge for all $s = \sigma + i t$ where $\sigma > \sigma_0$.

Proof:
We begin with a lemma:
Theorem: Existence of Abscissa of Convergence/General

Let $s = \sigma + i t$
Let $\ds \map f s = \sum_{n \mathop = 1}^\infty a_n e^{-\lambda_n s}$ be a general Dirichlet series.
Then there exists a extended real number, $\sigma_0$, such that
:$(1): \quad$ For $\sigma < \sigma_0$, $\map f s$ diverges
:$(2): \quad$ For $\sigma > \sigma_0$, $\map f s$ converges.

Proof:
If there does not exist an $s_0$ such that $\map f {s_0}$ converges, then $\sigma_0 = \infty$ and the theorem is vacuously true
If there does exist such an $s_0$, let $\sigma_0$ be the infimum of the real part of all such $s_0$, where $\sigma_0= -\infty$ if the set is not bounded from below.
*It is clear that $\map f s$ diverges if $\sigma < \sigma_0$ by construction of $\sigma_0$ as the infimum of all convergent $s$
*As $\sigma_0$ is the infimum of the the real part of the set all s such that $\map f s$ converges, for any $\epsilon > 0$, there exists an $s$ such that $\map f s$ converges and $\sigma_0 \le \sigma < \sigma_0+ \epsilon$ as otherwise $\sigma_0 + \epsilon$ would be the infimum of the set. 
:Therefore, for any $s$ such that $\sigma > \sigma_0$, we can pick $\epsilon = \sigma - \sigma_0$ and find a $q$ such that $\map f q$ converges and $\map \Re q < \sigma$.
:By Dirichlet Series Convergence Lemma, We therefore have that $\map f s$ converges.
{{qed}}
Category:General Dirichlet Series
9wmlqg29wilxnk1rcd69dsh990m6gt3
Theorem: Difference of Abscissae of Convergence

Let $\ds \map f s = \sum_{n \mathop = 1}^\infty a_n n^{-s}$ be a Dirichlet series.
Suppose that $\map f s$ has finite Abscissa of Convergence $\sigma_c$.
Then the Abscissa of Absolute Convergence $\sigma_a$ is finite, and:
:$0 \le \sigma_a - \sigma_c \le 1$

Proof:
It is trivial that $\sigma_a \ge \sigma_c$.
Suppose $s_0 = \sigma_0 + i t_0 \in \C$ such that $\map f {s_0}$ converges.
It is sufficient to show that $\map f s$ converges absolutely for all $s = \sigma + i t$ with $\sigma > \sigma_0 + 1$.
Pick an upper bound $M$ for the real numbers $\size {a_n n^{-s_0} }$.
Then for $s = \sigma + i t$ with $\sigma > \sigma_0 + 1$:
:$\size {\dfrac {a_n} {n^s} } = \size {\dfrac {a_n} {n^{s_0} n^{s - s_0} } } = \dfrac M {n^{\sigma - \sigma_0} }$
Then by the Comparison Test, $\ds \sum_{n \mathop = 1}^\infty \size {a_n n^{-s} }$ converges.
{{qed}}
Theorem: Completion Theorem (Metric Space)

Let $M = \struct {A, d}$ be a metric space.
Then there exists a completion $\tilde M = \struct {\tilde A, \tilde d}$ of $\struct {A, d}$.
Moreover, this completion is unique up to isometry.
That is, if $\struct {\hat A, \hat d}$ is another completion of $\struct {A, d}$, then there is a bijection $\tau: \tilde A \leftrightarrow \hat A$ such that:
{{begin-itemize}}
{{item|(1):|$\tau$ restricts to the identity on $x$:
$\forall x \in A: \map \tau x {{=}} x$}}
{{item|(2):|$\tau$ preserves metrics:
$\forall x_1, x_2 \in A : \map {\hat d} {\map \tau {x_1}, \map \tau {x_2} } {{=}} \map {\tilde d} {x_1, x_2}$}}
{{end-itemize}}

Proof:
We construct the completion of a metric space as equivalence classes of the set of Cauchy sequences in the space under a suitable equivalence relation.
Let $\struct {A, d}$ be a metric space.
Let $\CC \sqbrk A$ denote the set of all Cauchy sequences in $A$.
Define a relation $\sim$ on $\CC \sqbrk A$ by:
:$\ds \sequence {x_n} \sim \sequence {y_n} \iff \lim_{n \mathop \to \infty} \map d {x_n, y_n} = 0$
By Equivalence Relation on Cauchy Sequences, $\sim$ is an equivalence relation on $\CC \sqbrk A$.
Denote the equivalence class of $\sequence {x_n} \in \CC \sqbrk A$ by $\eqclass {x_n} \sim$.
Denote the set of equivalence classes under $\sim$ by $\tilde A$.
By Relation Partitions Set iff Equivalence this is a partition of $\CC \sqbrk A$.
That is, each $\sequence {x_n} \in \CC \sqbrk A$ lies in one and only one equivalence class under $\sim$.
Define $\tilde d: \tilde A \to \R_{\ge 0}$ by:
:$\ds \map {\tilde d} {\eqclass {x_n} \sim, \eqclass {y_n} \sim} = \lim_{n \mathop \to \infty} \map d {x_n, y_n}$
Theorem: Completeness Criterion (Metric Spaces)

Let $M = \struct {S, d}$ be a metric space.
Let $A \subseteq S$ be a dense subset.
Suppose that every Cauchy sequence in $A$ converges in $M$.
Then $M$ is complete.

Proof:
Let $\sequence {x_n}_{n \mathop \in \N}$ be a Cauchy sequence in $S$.
For each $n$ pick a Cauchy sequence $\sequence {y_{n, m} }_{m \mathop \in \N}$ in $A$ converging to $x_n$ like so:
:400pxCaption
Let $N \in \N$ be such that $\map d {x_{n_1}, x_{n_2} } < \epsilon / 3$ for all $n_1, n_2 > N$.
Let $M \in \N$ be such that $\map d {y_{n_i, m}, x_{n_i} } < \epsilon / 3$ for all $m > M$ and all $n_1, n_2 > N$. 
Let $m > M$.
Let $n_1, n_2 > N$.
We have:
{{begin-eqn}}
{{eqn | l = \map d {y_{n_1, m}, y_{n_2, m} }
      | o = \le
      | r = \map d {y_{n_1, m}, x_{n_1} } + \map d {x_{n_1}, x_{n_2} } + \map d {x_{n_2}, y_{n_2, m} }
      | c = two applications of the Triangle Inequality
}}
{{eqn | o = <
      | r = \epsilon
}}
{{end-eqn}}
Therefore $\sequence {y_{m, n} }_{n \mathop \in \N}$ is Cauchy in $A$ for $m > M$.
So $\sequence {y_{m, n} }_{n \mathop \in \N}$ converges to some limit $y_n \in S$.
{{finish|Proof to complete}}
Theorem: Completeness Criterion (Metric Spaces)

Let $M = \struct {S, d}$ be a metric space.
Let $A \subseteq S$ be a dense subset.
Suppose that every Cauchy sequence in $A$ converges in $M$.
Then $M$ is complete.

Proof:
Let $\left\langle{x_n}\right\rangle$ be a Cauchy sequence in $M$.
Since $A$ is dense, we can invoke the Axiom of Countable Choice to choose for each $n$ some $y_n \in A$ which is within $1 / n$ of $x_n$.
We will show that $\left\langle{y_n}\right\rangle$ is Cauchy.
Let $\epsilon > 0$.
Since $\left\langle{x_n}\right\rangle$ is Cauchy, there exists some $N'$ such that:
:$\forall n, m \ge N': d \left({x_n, x_m}\right) < \frac 1 3 \epsilon$
Let $N \in \N$ be greater than $N'$ and $3 \epsilon^{-1}$.
Note that $n, m \ge N$ implies that both:
: $(1): \quad n, m \ge N'$
: $(2): \quad \dfrac 1 n, \dfrac 1 m \le \dfrac 1 N < \dfrac 1 3 \epsilon$
Thus for $n, m \ge N$, by the Triangle Inequality and the above:
{{begin-eqn}}
{{eqn | l = d \left({y_n, y_m}\right)
      | o = \le
      | r = d \left({y_n, x_n}\right) + d \left({x_n, x_m}\right) + d \left({x_m, y_m}\right)
      | c = 
}}
{{eqn | o = <
      | r = \frac 1 n + \frac 1 3 \epsilon + \frac 1 m 
      | c = 
}}
{{eqn | o = <
      | r = \frac 1 3 \epsilon + \frac 1 3 \epsilon + \frac 1 3 \epsilon
      | c = 
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
Hence $\left\langle{y_n}\right\rangle$ is a Cauchy sequence in $A$.
By assumption, it converges to some limit $y \in S$.
Now, we verify that $\left\langle{x_n}\right\rangle$ converges to $y$ as well.
Let $\epsilon > 0$.
Since $\left\langle{y_n}\right\rangle$ converges, there exists some $N'$ such that:
:$\forall n \ge N': d \left({y_n, y}\right) < \dfrac 1 2 \epsilon$
Let $N \in \N$ be greater than $N'$ and $2 \epsilon^{-1}$.
Note that $n \ge N$ implies that both:
: $(1): \quad n \ge N'$
: $(2): \quad \dfrac 1 n \le \dfrac 1 N < \dfrac 1 2 \epsilon$
Thus, for $n \ge N$, we have by the Triangle Inequality and above that:
{{begin-eqn}}
{{eqn | l = d \left({x_n, y}\right)
      | o = \le
      | r = d \left({x_n, y_n}\right) + d \left({y_n, y}\right)
      | c = 
}}
{{eqn | o = <
      | r = \frac 1 n + \frac 1 2 \epsilon
      | c = 
}}
{{eqn | o = <
      | r = \frac 1 2 \epsilon + \frac 1 2 \epsilon
      | c = 
}}
{{eqn | r = \epsilon
      | c = 
}}
{{end-eqn}}
Hence $\left\langle{x_n}\right\rangle$ converges to $y$.
{{qed}}
Theorem: Natural Number Addition is Closed

The operation of addition on the set of natural numbers $\N$ is closed:
:$\forall x, y \in \N: x + y \in \N$

Proof:
Follows directly from Natural Numbers under Addition form Commutative Monoid.
A monoid by definition is a semigroup.
Again by definition, the operation in a semigroup is closed.
{{qed}}
Theorem: Characterisation of Ordered Fields

Let $\struct {k, +, \cdot}$ be a field with unity $1$ and zero $0$.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|There exists a total ordering $\le$ on $k$ such that $\struct {k, \le}$ is an ordered field}}
{{item|(2):|$-1$ cannot be written as a sum of squares of elements of $k$}}
{{item|(3):|$0$ cannot be written as a non-empty sum of squares of non-zero elements of $k$}}
{{end-itemize}}

Proof:
=== $(2)$ iff $(3)$ ===
Suppose there exist $\set {x_i: i \in I}$ such that
:$\ds -1 = \sum_{i \mathop \in I} x_i^2$
Then
:$\ds 0 = 1^2 + \sum_{i \mathop \in I} x_i^2$
a non-empty sum of non-zero squared of $k$.
Conversely, suppose that there is a set $\set {x_i: i \in I} \ne \O$ with $x_i \ne 0$ for all $i \in I$ such that:
:$\ds 0 = \sum_{i \mathop \in I} x_i^2$
Then for any $j \in I$:
:$\ds -x_j^2 = \sum_{\substack {i \mathop \in I \\ i \mathop \ne j} } x_i^2$
Dividing through by $x_j^2$ we find that:
:$\ds -1 = -\paren {\frac {x_j} {x_j} }^2 = \sum_{\substack {i \mathop \in I \\ i \mathop \ne j} } \paren {\frac {x_i} {x_j} }^2$
Theorem: Hahn-Banach Theorem/Real Vector Space

Let $X$ be a vector space over $\R$. 
Let $p : X \to \R$ be a sublinear functional.
Let $X_0$ be a linear subspace of $X$. 
Let $f_0 : X_0 \to \R$ be a linear functional such that: 
:$\map {f_0} x \le \map p x$ for each $x \in X_0$. 
Then there exists a linear functional $f$ defined on the whole space $X$ which extends $f_0$ and satisfies: 
:$\map f x \le \map p x$ for each $x \in X$.
That is, there exists a linear functional $f : X \to \R$ such that: 
:$\map f x \le \map p x$ for each $x \in X$
and:
:$\map f x = \map {f_0} x$ for each $x \in X_0$.

Proof:
We first prove a lemma:
Theorem: Completion of Valued Field

Let $\struct {k, \norm {\,\cdot\,} }$ be a valued field.
Then there exists a completion $\struct {k', \norm {\,\cdot\,}'}$ of $\struct {k, \norm {\,\cdot\,} }$ such that $\struct {k', \norm {\,\cdot\,}'}$ is a valued field.
Furthermore, every completion of $\struct{k, \norm {\,\cdot\,} }$ is isometrically isomorphic to $\struct {k', \norm {\,\cdot\,}'}$.

Proof:
By Completion of Normed Division Ring then $\struct {k, \norm {\, \cdot \,} }$ has a normed division ring completion $\struct {k', \norm {\, \cdot \,}'}$
By Normed Division Ring is Field iff Completion is Field then $\struct {k', \norm {\, \cdot \,}'}$ is a field.
By Normed Division Ring Completions are Isometric and Isomorphic then every completion of $\struct {k, \norm {\,\cdot\,} }$ is isometrically isomorphic to $\struct {k', \norm {\,\cdot\,}'}$.
{{qed}}
Theorem: Hardy-Littlewood Circle Method

Let $\AA$ be a subset of the non-negative integers.
Let:
:$\ds \map T s = \sum_{a \mathop \in \AA} s^a$
be the generating function for $\AA$.
For $N \in \N$, let $\map {r_{\AA, \ell} } N$ be the number of solutions $\tuple {x_1, \ldots, x_\ell} \in \AA^\ell$ to the equation:
:$x_1 + \cdots + x_\ell = N$
Then:
:$\ds \forall \rho \in \openint 0 1: \map {r_{\AA, \ell} } N = \oint_{\size s \mathop = \rho} \frac {\map T s^\ell} {s^{N + 1} } \rd s$

Proof:
We have:
:$\ds \map T s^\ell = \sum_{N \mathop = 0}^\infty \map {r_{\AA, \ell} } N s^N$
and:
:$\map {\dfrac {\d^N} {\d s^N} } {\map T s^\ell} = N! \cdot \map {r_{\AA, \ell} } N + \map \OO s$
so:
:$\map {r_{\AA, \ell} } N = \dfrac 1 {N!} \dfrac {\d^N} {\d s^N} \bigintlimits {\map T s^\ell} {s \mathop = 0}{}$
Now recall Cauchy's Integral Formula for Derivatives for a complex function $f$ holomorphic on a domain $D$, and a path $\gamma \subseteq D$ winding once around $a$:
:$\ds \valueat {\frac {\d^N} {\d s^N} \map f s} {s \mathop = a} = \frac {N!} {2 \pi i} \oint_\gamma \frac {\map f s} {\paren {s - a}^{N + 1} } \rd s$
Since $\map T s$ is defined by a generating function, $\map T s^\ell$ has a Taylor series about $s = 0$ which converges for all $\size s < 1$.
Applying Cauchy's formula:
{{begin-eqn}}
{{eqn | l = \map {r_{\AA, \ell} } N
      | r = \frac 1 {N!} \frac {\d^N} {\d s^N} \bigintlimits {\map T s^\ell} {s \mathop = 0} {}
}}
{{eqn | r = \frac 1 {2 \pi i} \oint_\gamma \frac {\map T s^\ell} {s^{N + 1} } \rd s
}}
{{end-eqn}}
where $\gamma$ a circle about zero of radius $\rho$ for any $\rho < 1$.
{{qed}}
{{Namedfor|Godfrey Harold Hardy|name2 = John Edensor Littlewood|cat = Hardy|cat2 = Littlewood}}
{{explain|Plenty of links to be included and explanations to be added.}}
Category:Analytic Number Theory
7zwpyb730weq9y0pdp90cfz2n0g9yvp
Theorem: Vinogradov Circle Method

Let $\AA$ be a subset of the non-negative integers.
For $\alpha \in \R$, let:
:$\map e \alpha := \map \exp {2 \pi i \alpha}$
Let:
:$\ds \map {T_N} s = \sum_{\substack {a \mathop \in \AA \\ a \mathop \le N} } s^a$
be the truncated generating function for $\AA$.
{{explain|"truncated" generating function}}
Let:
:$\map {V_N} \alpha := \map {T_N} {\map e \alpha}$
Let $\map {r_{\AA, \ell} } N$ be the number of solutions $\tuple {x_1, \dotsc, x_\ell} \in \AA^\ell$ to the equation:
:$(1): \quad x_1 + \cdots + x_l = N$
Then:
:$\ds \map {r_{\AA, \ell} } N = \int_0^1 \map {V_N} \alpha^\ell \map e {-N \alpha} \rd \alpha$

Proof:
For $m \in \N$ let $\map {r_{\AA, \ell} } {m; N}$ be the number of solutions to $(1)$ with no $x_i$ exceeding $N$.
Then:
:$\forall m \le N: \map {r_{\AA, \ell} } {m; N} = \map {r_{\AA, \ell} } m$
and:
:$\forall m > \ell N: \map {r_{\AA, \ell} } {m; N} = 0$
Then we compute:
:$\ds \map {T_N} s^\ell = \sum_{m \mathop = 0}^{\ell N} \map {r_{\AA, \ell} } {m; N} s^m$
and:
:$(2): \quad \ds \map {V_N} \alpha^\ell = \sum_{m \mathop = 0}^{\ell N} \map {r_{\AA, \ell} } {m; N} \map e {\alpha m}$
Now it follows from Exponentials Form Orthonormal Basis for $\LL^2$ that:
:$\ds \int_0^1 \map e {\alpha m} \map e {-\alpha n} \rd \alpha = \delta_{m n}$
where $\delta_{m n}$ is the Kronecker delta.
Therefore, we multiply $(2)$ by $\map e {-N \alpha}$ and integrate:
:$\ds \map {r_{\AA, \ell} } N = \map {r_{\AA, \ell} } {N; N} = \int_0^1 \map {V_N} \alpha^\ell \map e {-N \alpha} \rd \alpha$
{{qed}}
{{Namedfor|Ivan Matveevich Vinogradov|cat = Vinogradov I M}}
Category:Analytic Number Theory
t2y7zdqz5x6vi1phu2aymujsq1y4ue5
Theorem: Correspondence between Linear Group Actions and Linear Representations

Let $\struct {k, +, \cdot}$ be a field.
Let $V$ be a vector space over $k$ of finite dimension.
Let $\struct {G, *}$ be a finite group.
There is a one-to-one correspondence between linear group actions of $G$ on $V$ and linear representations of $G$ in $V$, as follows:
Let $\phi: G \times V \to V$ be a group action.
Let $\rho: G \to \map {\operatorname {Sym} } V$ be a permutation representation of $G$ on $V$.
The following are equivalent:
:$(1): \quad$ $\rho$ is the permutation representation associated to $\phi$
:$(2): \quad$ $\phi$ is the group action associated to $\rho$
If this is the case, the following are equivalent:
:$(1): \quad$ $\rho$ is a linear representation
:$(2): \quad$ $\phi$ is a linear group action

Proof:
The first equivalence follows from Correspondence Between Group Actions and Permutation Representations.
Theorem: Set Difference with Disjoint Set

Let $S, T$ be sets.
Then:
:$S \cap T = \O \iff S \setminus T = S$
where:
:$S \cap T$ denotes set intersection
:$\O$ denotes the empty set
:$S \setminus T$ denotes set difference.

Proof:
{{begin-eqn}}
{{eqn | l = S \cap T
      | r = \O
}}
{{eqn | ll= \leadstoandfrom
      | l = S
      | o = \subseteq
      | r = \map \complement T
      | c = Intersection with Complement is Empty iff Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = S \cap \map \complement T
      | r = S
      | c = Intersection with Subset is Subset
}}
{{eqn | ll= \leadstoandfrom
      | l = S \setminus T
      | r = S
      | c = Set Difference as Intersection with Complement
}}
{{end-eqn}}
{{qed}}
Theorem: Integer Subtraction is Closed

The set of integers is closed under subtraction:
:$\forall a, b \in \Z: a - b \in \Z$

Proof:
From the definition of subtraction:
:$a - b := a + \paren {-b}$
where $-b$ is the inverse for integer addition.
From Integers under Addition form Abelian Group, the algebraic structure $\struct {\Z, +}$ is a group.
Thus:
:$\forall a, b \in \Z: a + \paren {-b} \in \Z$
Therefore integer subtraction is closed.
{{qed}}
Theorem: Rational Subtraction is Closed

The set of rational numbers is closed under subtraction:
:$\forall a, b \in \Q: a - b \in \Q$

Proof:
From the definition of subtraction:
:$a - b := a + \paren {-b}$
where $-b$ is the inverse for rational number addition.
From Rational Numbers under Addition form Infinite Abelian Group, $\struct {\Q, +}$ forms a group.
Thus:
:$\forall a, b \in \Q: a + \paren {-b} \in \Q$
Therefore rational number subtraction is closed.
{{qed}}
Theorem: Real Subtraction is Closed

The set of real numbers is closed under subtraction:
:$\forall a, b \in \R: a - b \in \R$

Proof:
From the definition of real subtraction:
:$a - b := a + \paren {-b}$
where $-b$ is the inverse for real number addition.
From Real Numbers under Addition form Group:
:$\forall a, b \in \R: a + \paren {-b} \in \R$
Therefore real number subtraction is closed.
{{qed}}
Theorem: Complex Subtraction is Closed

The set of complex numbers is closed under subtraction:
:$\forall a, b \in \C: a - b \in \C$

Proof:
From the definition of complex subtraction:
:$a - b := a + \paren {-b}$
where $-b$ is the inverse for complex number addition.
From Complex Numbers under Addition form Group, it follows that:
:$\forall a, b \in \C: a + \paren {-b} \in \C$
Therefore complex number subtraction is closed.
{{qed}}
Theorem: Strictly Positive Real Numbers are Closed under Division

The set $\R_{>0}$ of strictly positive real numbers is closed under division:
:$\forall a, b \in \R_{>0}: a \div b \in \R_{>0}$

Proof:
From the definition of division:
:$a \div b := a \times \paren {\dfrac 1 b}$
where $\dfrac 1 b$ is the inverse for real number multiplication.
From Strictly Positive Real Numbers under Multiplication form Uncountable Abelian Group, the algebraic structure $\struct {\R_{>0}, \times}$ forms a group.
Thus it follows that:
:$\forall a, b \in \R_{>0}: a \times \paren {\dfrac 1 b} \in \R$
Therefore real number division is closed in $\R_{>0}$.
{{qed}}
Theorem: Rational Numbers form Integral Domain

The set of rational numbers $\Q$ forms an integral domain under addition and multiplication: $\struct {\Q, +, \times}$.

Proof:
Recall that Rational Numbers form Field.
The result then follows directly from Field is Integral Domain.
{{qed}}
Theorem: Real Numbers form Integral Domain

The set of real numbers $\R$ forms an integral domain under addition and multiplication: $\struct {\R, +, \times}$.

Proof:
Recall that Real Numbers form Field.
The result then follows directly from Field is Integral Domain.
{{qed}}
Theorem: Complex Numbers form Integral Domain

The set of complex numbers $\C$ forms an integral domain under addition and multiplication: $\struct {\C, +, \times}$.

Proof:
Recall that Complex Numbers form Field.
The result then follows directly from Field is Integral Domain.
{{qed}}
Theorem: Gauss's Lemma on Unique Factorization Domains

Let $R$ be a unique factorization domain.
Then the ring of polynomials $R \sqbrk X$ is also a unique factorization domain.

Proof:
{{ProofWanted|this possibly works}}
{{Namedfor|Carl Friedrich Gauss|cat = Gauss}}
Category:Factorization
Category:Unique Factorization Domains
nhk280w723paxiql05rzkp23k6sghaq
Theorem: Product with Inverse equals Identity iff Equality

Let $\struct {G, \circ}$ be a group whose identity element is $e$.
Then:
:$\forall a, b \in G: a \circ b^{-1} = e \iff a = b$

Proof:
Using various properties of groups:
{{begin-eqn}}
{{eqn | l = a \circ b^{-1}
      | r = e
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {a \circ b^{-1} } \circ b
      | r = e \circ b
      | c = Cancellation Laws
}}
{{eqn | ll= \leadstoandfrom
      | l = a \circ \paren {b^{-1} \circ b}
      | r = e \circ b
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = a
      | r = b
      | c = {{Group-axiom|2}} and {{Group-axiom|3}}
}}
{{end-eqn}}
{{qed}}
Category:Group Theory
c8d3icn9qmt7gena811yk1ggzi3bvnb
Theorem: Gröbner Basis

Let $F$ be a finite set of polynomials.
{{explain|Explain what the underlying field of the polynomials is. Real numbers, abstract rings, general fields? Link to the appropriate definition for the case.}}
Let $\map {\operatorname {SP} } {f_1, f_2}$ be the $S$-polynomial of $f_1$ and $f_2$.
Let $g$ be a polynomial.
Let $\map {\operatorname {RF} } g$ be the reduced form of $g$.
Then $F$ is a Gröbner basis {{iff}}:
:$\forall f_1, f_2 \in \map F {\map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } = 0}$
{{explain|The meaning of the above needs to be made clear. Presumably it should be interpreted something like: $\forall f_1, f_2 \in F: \map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } {{=}} 0$. But further to this: $RF$ as defined takes a single argument, a polynomial (still to be defined upon what domain). As this statement stands, $RF$ seems to take two parameters: $F$ and $\operatorname {SP}$. Clarification is needed.}}

Proof:
=== Necessary Condition ===
Let $F$ be a Gröbner basis.
Let $f_1, f_2 \in F$.
Then:
:$\map {\operatorname {SP} } {f_1, f_2} \in \map {\operatorname {Ideal} } F$
That is:
:$\map {\operatorname {SP} } {f_1, f_2} \equiv_F 0$
{{explain|Link to a result explaining the above.}}
By the relation between reduction and congruence this implies that:
:$\map {\operatorname {SP} } {f_1, f_2} \leftrightarrow_F^* 0$
{{explain|Define via links to the appropriate pages the meaning of the above.}}
Hence:
:$\map {\operatorname {RF} } {F, \map {\operatorname {SP} } {f_1, f_2} } = \map {\operatorname {RF} } {F, 0} = 0$ 
because $F$ is a Gröbner basis (and because of the equivalence
between the Church-Rosser property and the normal form Church-Rosser property).
{{explain|Establish the above equivalence and the conclusion drawn from it in a separate page.}}
{{qed|lemma}}