nyuuzyou/wikis huggingface dataset:
Definite Integral to Infinity of Reciprocal of x Squared plus a Squared/Corollary

== Theorem ==
:$\ds \int_0^\infty \dfrac {\d x} {1 + x^2} = \frac \pi 2$
for $a \ne 0$. 
== Proof ==
From Definite Integral to Infinity of Reciprocal of x Squared plus a Squared:
:$\ds \int_0^\infty \dfrac {\d x} {x^2 + a^2} = \frac \pi {2 a}$
which holds for for $a \ne 0$. 
The result follows by setting $a = 1$.
== Sources ==
* : $1.1$ What is asymptotics? $(1.1.1)$
Category:Definite Integral to Infinity of Reciprocal of x Squared plus a Squared
Category:Definite Integrals involving x squared plus a squared
Definite Integral to Infinity of Reciprocal of x Squared plus a Squared/Proof 3

== Theorem ==
== Proof == 
Let $C_R$ be the semicircular contour of radius $R$ situated on the upper half plane, centred at the origin, traversed anti-clockwise.
Let $\Gamma_R = C_R \cup \closedint {-R} R$.
Then, by Contour Integral of Concatenation of Contours:
:$\ds \oint_{\Gamma_R} \frac {\d z} {z^2 + a^2} = \int_{C_R} \frac {\d z} {z^2 + a^2} + \int_{-R}^R \frac {\d x} {x^2 + a^2}$
we have: 
from which:
:$\ds \lim_{R \mathop \to \infty} \oint_{\Gamma_R} \frac {\d z} {z^2 + a^2} = \lim_{R \mathop \to \infty} \int_{-R}^R \frac {\d x} {x^2 + a^2} = \int_{-\infty}^\infty \frac {\d x} {x^2 + a^2}$
The integrand is meromorphic.
So by Cauchy's Residue Theorem:
:$\ds \lim_{R \mathop \to \infty} \oint_{\Gamma_R} \frac {\d z} {z^2 + a^2} = 2 \pi i \sum \Res {\frac 1 {z^2 + a^2} } {z_0}$
where the summation runs over the poles of $\dfrac 1 {z^2 + a^2}$.
The integrand can be written as:
:$\dfrac 1 {\paren {z - a i} \paren {z + a i} }$
From this it can be observed that the integrand has only two simple poles: $z_0 = a i$ and $z_0 = -a i$.
Only the former of these lies in the contour, so:
So: 
:$\ds \int_{-\infty}^\infty \frac {\d x} {x^2 + a^2} = \frac \pi a$
From Definite Integral of Even Function:
:$\ds \int_{-\infty}^\infty \frac {\d x} {x^2 + a^2} = 2 \int_0^\infty \frac {\d x} {x^2 + a^2}$
Hence: 
:$\ds \int_0^\infty \frac {\d x} {x^2 + a^2} = \frac \pi {2 a}$
Category:Definite Integral to Infinity of Reciprocal of x Squared plus a Squared
Definite Integral to Infinity of Sine m x over x by x Squared plus a Squared

== Theorem ==
:$\ds \int_0^\infty \frac {\sin m x} {x \paren {x^2 + a^2} } \rd x = \frac \pi {2 a^2} \paren {1 - e^{-m a} }$
where:
:$a$ is a positive real number
:$m$ is a non-negative real number.
== Proof ==
Fix $a$ and set: 
:$\ds \map I m = \int_0^\infty \frac {\sin m x} {x \paren {x^2 + a^2} } \rd x$
for $m \ge 0$. 
We have:
So by Primitive of $e^{a x}$:
:$\map I m = -\dfrac \pi {2 a^2} e^{-m a} + C$
for some constant $C \in \R$.
We have: 
On the other hand: 
So:
:$C = \dfrac \pi {2 a^2}$
giving: 
:$\ds \map I m = \int_0^\infty \frac {\sin m x} {x \paren {x^2 + a^2} } \rd x = \frac \pi {2 a^2} \paren {1 - e^{-m a} }$
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.42$
Category:Definite Integrals involving Sine Function
Definite Integral to Infinity of Sine of a x^2

== Theorem ==
:$\ds \int_0^\infty \map \sin {a x^2} \rd x = \frac 1 2 \sqrt {\frac \pi {2 a} }$
where $a$ is a positive real number. 
== Proof ==
We have, by Euler's Formula: Corollary:
:$\map \exp {-i a x^2} = -i \map \sin {a x^2} + \map \cos {a x^2}$
As $\map \sin {a x^2}$ and $\map \cos {a x^2}$ are both real for real $a, x$, we therefore have:
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.50$
Category:Definite Integrals involving Sine Function
Definite Integral to Infinity of Sine of a x over Hyperbolic Sine of b x

== Theorem ==
:$\ds \int_0^\infty \frac {\sin a x} {\sinh b x} \rd x = \frac \pi {2 b} \tanh \frac {a \pi} {2 b}$
where:
:$a$ and $b$ are positive real numbers
:$\tanh$ denotes the hyperbolic cotangent function.
== Proof ==
We have, as $b, n > 0$:
We similarly have:
So:
By Mittag-Leffler Expansion for Hyperbolic Tangent Function, we have: 
:$\ds \pi \map \tanh {\pi z} = 8 \sum_{n \mathop = 0}^\infty \frac z {4 z^2 + \paren {2 n + 1}^2}$
where $z$ is not a half-integer multiple of $i$. 
Setting $z = \dfrac a {2 b}$ gives: 
:$\ds \pi \map \tanh {\frac {a \pi} {2 b} } = 8 \sum_{n \mathop = 0}^\infty \frac {\paren {\frac a {2 b} } } {4 \paren {\frac a {2 b} }^2 + \paren {2 n + 1}^2}$
Therefore: 
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.112$
Category:Definite Integrals involving Hyperbolic Sine Function
Category:Definite Integrals involving Sine Function
Definite Integral to Infinity of Sine of m x over Exponential of 2 Pi x minus One

== Theorem ==
:$\ds \int_0^\infty \frac {\sin m x} {e^{2 \pi x} - 1} \rd x = \frac 1 4 \coth \frac m 2 - \frac 1 {2 m}$
where:
:$m$ is a non-zero real number
:$\coth$ is the hyperbolic cotangent function.
== Proof ==
We have:
By Mittag-Leffler Expansion for Hyperbolic Cotangent Function we have: 
:$\ds \sum_{k \mathop = 1}^\infty \frac z {k^2 + z^2} = \frac \pi 2 \map \coth {\pi z} - \frac 1 {2 z}$
for all $z \in \C$ where $z$ is not an integer multiple of $i$. 
Since all variables concerned in this instance all real-valued, we can apply this identity. 
Setting $z = \dfrac m {2 \pi}$ in the above we obtain:
So:
:$\ds \int_0^\infty \frac {\sin m x} {e^{2 \pi x} - 1} \rd x = \frac 1 {2 \pi} \paren {\frac \pi 2 \coth \frac m 2 - \frac \pi m} = \frac 1 4 \coth \frac m 2 - \frac 1 {2 m}$
as required.
== Sources ==
* : $\S 15$: Definite Integrals involving Exponential Functions: $15.83$
Category:Definite Integrals involving Sine Function
Category:Definite Integrals involving Exponential Function
Definite Integral to Infinity of Sine x over Root x

== Theorem ==
:$\ds \int_0^\infty \frac {\sin x} {\sqrt x} \rd x = \sqrt {\frac \pi 2}$
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.53$
Category:Definite Integrals involving Sine Function
Definite Integral to Infinity of x by Sine m x over x Squared plus a Squared

== Theorem ==
:$\ds \int_0^\infty \frac {x \sin m x} {x^2 + a^2} \rd x = \frac \pi 2 e^{-m a}$
where $m$ and $a$ are positive real numbers. 
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 15$: Definite Integrals involving Trigonometric Functions: $15.41$
Category:Definite Integrals involving Sine Function
Category:Definite Integral to Infinity of x by Sine m x over x Squared plus a Squared
Definite Integral to Infinity of x by Sine m x over x Squared plus a Squared/Proof 1

== Theorem ==
== Proof ==
From Definite Integral of Even Function:
:$\ds \frac 1 2 \int_{-\infty}^\infty \frac {x \sin m x} {x^2 + a^2} \rd x = \int_0^\infty \frac {x \sin m x} {x^2 + a^2} \rd x$
With the aim of integrating over the domain, we split the domain up into $2$ components as follows:
Let $R$ be a positive real number with $R > a$.
Let $C_1$ be the straight line segment from $-R$ to $R$.
Let $C_2$ be the arc of the circle of radius $R$ centred at the origin connecting $R$ and $-R$ anticlockwise.
Let $\Gamma = C_1 \cup C_2$. 
Let: 
:$\map f x = \dfrac {x e^{i m x} } {x^2 + a^2}$
From Euler's Formula, we have: 
:$\map f x = \dfrac {x \cos m x} {x^2 + a^2} + i \dfrac {x \sin m x} {x^2 + a^2}$
So:
Note that the integrand is meromorphic with simple poles where $x^2 + a^2 = 0$. 
That is, at $x = a i$ and $x = -a i$. 
As our semi-circular contour lies in the upper half-plane, the only pole of concern is $a i$.
As $R > a$, these poles do not lie on $C_2$, but are enclosed by the curve $\Gamma$.
We have:
 
The integral over $C_2$ can be shown to vanish as $R \to \infty$:
Taking $R \to \infty$, we have:
So: 
:$\ds \int_{-\infty}^\infty \frac {x \sin m x} {x^2 + a^2} \rd x = \pi e^{-m a}$
giving:
:$\ds \int_0^\infty \frac {x \sin m x} {x^2 + a^2} \rd x = \frac \pi 2 e^{-m a}$
Category:Definite Integral to Infinity of x by Sine m x over x Squared plus a Squared
Definite Integral to Infinity of x by Sine m x over x Squared plus a Squared/Proof 2

== Theorem ==
== Proof ==
From Definite Integral to Infinity of $\dfrac {\cos m x} {x^2 + a^2}$:
:$\ds \int_0^\infty \frac {\cos m x} {x^2 + a^2} \rd x = \frac \pi {2 a} e^{-m a}$
We have: 
So:
Category:Definite Integral to Infinity of x by Sine m x over x Squared plus a Squared
Definite Integral to Infinity of x over Exponential of x minus One

== Theorem ==
:$\ds \int_0^\infty \frac x {e^x - 1} \rd x = \frac {\pi^2} 6$
 
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Exponential Functions: $15.79$
Category:Definite Integrals involving Exponential Function
Definite Integral to Infinity of x over Exponential of x plus One

== Theorem ==
:$\ds \int_0^\infty \frac x {e^x + 1} \rd x = \frac {\pi^2} {12}$
 
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Exponential Functions: $15.81$
Category:Definite Integrals involving Exponential Function
Definite Integral to Infinity of x over Hyperbolic Sine of a x

== Theorem ==
:$\ds \int_0^\infty \frac x {\sinh a x} \rd x = \frac {\pi^2} {4 a^2}$
where $a$ is a positive real number.
== Proof ==
== Sources ==
* : $\S 15$: Definite Integrals involving Hyperbolic Functions: $15.114$
Category:Definite Integrals involving Hyperbolic Sine Function
Definition by Cases is Primitive Recursive

== Theorem ==
Let $\RR_1, \RR_2, \ldots, \RR_k$ be primitive recursive relations on $\N^l$ such that:
:$\forall i, j \in \set{1, 2, \ldots, k}: \RR_i \implies \lnot \RR_j$, that is, all relations are mutually exclusive
:$\forall \tuple {n_1, n_2, \ldots, n_l} \in \N^l: \exists i \in \set {1, 2, \ldots, k}: \map {\RR_i} {n_1, n_2, \ldots, n_l}$, that is, the set of relations is exhaustive.
Let $\forall i \in \set {1, 2, \ldots, k}: g_i: \N^l \to \N$ be primitive recursive functions.
Then the function $f: \N^l \to \N$ defined as:
$\quad \map f {n_1, n_2, \ldots, n_l} = \begin{cases}
\map {g_1} {n_1, n_2, \ldots, n_l} & : \map {\RR_1} {n_1, n_2, \ldots, n_l} \\
\map {g_2} {n_1, n_2, \ldots, n_l} & : \map {\RR_2} {n_1, n_2, \ldots, n_l} \\
\quad \vdots & \quad \vdots \\
\map {g_k} {n_1, n_2, \ldots, n_l} & : \map {\RR_k} {n_1, n_2, \ldots, n_l}
\end{cases}$
is primitive recursive.
=== Corollary ===
The definition can be made more flexible by defining $f$ as follows:
== Proof ==
We have:
 
because if $\tuple {n_1, n_2, \ldots, n_l} \in \N^k$, there is a unique $r$ such that $\map {\RR_r} {n_1, n_2, \ldots, n_l}$.
Then $\map {\chi_{\RR_r} } {n_1, n_2, \ldots, n_l} = 1$ and $\map {\chi_{\RR_s} } {n_1, n_2, \ldots, n_l} = 0$ for $s \ne r$.
Then the value of the is $\map {g_r} {n_1, n_2, \ldots, n_l}$ as required.
Since $\RR_1, \RR_2, \ldots, \RR_k$ are primitive recursive, the functions $\chi_{\RR_1}, \chi_{\RR_2}, \ldots, \chi_{\RR_k}$ are primitive recursive as well.
Hence $f$ is obtained by substitution from:
:the primitive recursive function $\operatorname{add}$
:the primitive recursive functions $g_j$
:the primitive recursive functions $\chi_{\RR_j}$.
Hence the result.
Category:Primitive Recursive Functions
Category:Definition by Cases is Primitive Recursive
Definition by Cases is Primitive Recursive/Corollary

== Corollary to Definition by Cases is Primitive Recursive ==
Let $\RR_1, \RR_2, \ldots, \RR_k$ be primitive recursive relations on $\N^l$ such that:
:$\forall i, j \in \set{1, 2, \ldots, k}: \RR_i \implies \lnot \RR_j$, that is, all relations are mutually exclusive
:$\forall \tuple {n_1, n_2, \ldots, n_l} \in \N^l: \exists i \in \set {1, 2, \ldots, k}: \map {\RR_i} {n_1, n_2, \ldots, n_l}$, that is, the set of relations is exhaustive.
Let $\forall i \in \set {1, 2, \ldots, k}: g_i: \N^l \to \N$ be primitive recursive functions.
Let $f: \N^l \to \N$ be defined as:
$\quad \map f {n_1, n_2, \ldots, n_l} = \begin {cases}
\map {g_1} {n_1, n_2, \ldots, n_l} & : \map {\RR_1} {n_1, n_2, \ldots, n_l} \\
\map {g_2} {n_1, n_2, \ldots, n_l} & : \map {\RR_2} {n_1, n_2, \ldots, n_l} \\
\quad \vdots & \quad \vdots \\
\map {g_{k - 1} } {n_1, n_2, \ldots, n_l} & : \map {\RR_{k - 1} } {n_1, n_2, \ldots, n_l} \\
\map {g_k} {n_1, n_2, \ldots, n_l} & : \text {otherwise}
\end {cases}$
where "otherwise" can be replaced by:
:$\map {\RR_k} {n_1, n_2, \ldots, n_l} = \lnot \paren {\map {\RR_1} {n_1, n_2, \ldots, n_l} \lor \map {\RR_2} {n_1, n_2, \ldots, n_l} \lor \ldots \lor \map {\RR_{k - 1} } {n_1, n_2, \ldots, n_l} }$
Thus we need to define only $k - 1$ mutually exclusive relations as the "otherwise" case takes care of the default case.
== Proof ==
Immediate from Definition by Cases is Primitive Recursive and Set Operations on Primitive Recursive Relations.
Category:Definition by Cases is Primitive Recursive
Definition of Polynomial from Polynomial Ring over Sequences

== Theorem ==
Let $\struct {R, +, \circ}$ be a ring with unity.
Let $\struct {P \sqbrk R, \oplus, \odot}$ be the polynomial ring over the set of all sequences in $R$:
:$P \sqbrk R = \set {\sequence {r_0, r_1, r_2, \ldots} }$
where the operations $\oplus$ and $\odot$ on $P \sqbrk R$ be defined as:
Let $\struct {R \sqbrk X, +, \circ}$ be the ring of polynomials over $R$ in $X$.
Then $\struct {R \sqbrk X, +, \circ}$ and $\struct {P \sqbrk R, \oplus, \odot}$ are isomorphic.
== Proof ==
Let $P \sqbrk R$ be the polynomial ring over $R$.
Consider the injection $\phi: R \to P \sqbrk R$ defined as:
:$\forall r \in R: \map \phi r = \sequence {r, 0, 0, \ldots}$
It is easily checked that $\phi$ is a ring monomorphism.
So the set $\set {\sequence {r, 0, 0, \ldots}: r \in R}$ is a subring of $P \sqbrk R$ which is isomorphic to $R$.
So we identify $r \in R$ with the sequence $\sequence {r, 0, 0, \ldots}$.
Next we note that $P \sqbrk R$ contains the element $\sequence {0, 1, 0, \ldots}$ which we can call $x$.
From the definition of ring product on the polynomial ring over $R$, we have that:
:$x^2 = \sequence {0, 1, 0, \ldots} \odot \sequence {0, 1, 0, \ldots} = \sequence {0, 0, 1, 0, 0, \ldots}$
:$x^3 = \sequence {0, 0, 1, 0, 0, \ldots} \odot \sequence {0, 1, 0, \ldots} = \sequence {0, 0, 0, 1, 0, \ldots}$
and in general:
:$x^n = \sequence {0, 1, 0, \ldots}^{n - 1} \odot \sequence {0, 1, 0, \ldots} = \sequence {0, \ldots \paren n \ldots, 0, 1, 0, \ldots}$
for all $n \ge 1$.
Hence we see that:
So by construction, $R \sqbrk X$ is seen to be equivalent to $P \sqbrk R$.
It can also be shown that this proof works for the general ring whether it be a ring with unity or not.
== Sources ==
* : Chapter $6$: Polynomials and Euclidean Rings: $\S 25$. Polynomials
Category:Ring Theory
Category:Polynomial Theory
Definitional Abbreviation/Examples

== Examples of Definitional Abbreviations ==
An example of a definitional abbreviation in predicate logic is to write:
:$\exists! x: \map \phi x$
in place of the formally correct alternatives:
:$\exists x: \paren {\map \phi x \land \forall y: \paren {\map \phi y \implies x = y} }$
:$\exists x: \forall y: \paren {\map \phi y \iff x = y}$
to express:
:there exists a unique $x$ such that $\map \phi x$ holds
where $\phi$ is some unary predicate symbol.
The benefit of this uniqueness quantifier readily becomes apparent when $\phi$ is already a very long formula in itself.
Two examples of definitional abbreviations in predicate logic are the restricted universal quantifier:
:$\forall x \in A: \map P x$
for:
:$\forall x: \paren {x \in A \implies \map P x}$
and the restricted existential quantifier:
:$\exists x \in A: \map P x$
for:
:$\exists x: \paren {x \in A \land \map P x}$
Category:Definitional Abbreviations
Degenerate Linear Operator Plus Identity is Fredholm Operator

== Theorem ==
Let $U$ be a vector space.
Let $T : U \to U$ be a degenerate linear operator.
Let $I_U : U \to U$ be the identity operator.
Then:
:$T + I_U$
is a Fredholm operator.
== Proof ==
We need to show that both:
:$\map \ker {T + I_U}$
and:
:$U / {\Img {T + I_U} }$
are finite-dimensional.
=== Proof of $\map \dim {\map \ker {T + I_U} } < +\infty$ ===
Let $u \in \map \ker {T + I_U}$.
That is:
:$Tu + u = 0$
Thus:
:$u = \map T {-u} \in \Img T$
Hence:
:$\map \ker {T + I_U} \subseteq \Img T$
Therefore:
=== Proof of $\map \dim {U / {\Img {T + I_U} } } < +\infty$ ===
Observe that:
:$\map \ker T \subseteq \Img {T + I_U}$
since if $u \in \map \ker T$, then:
:$u = T u + u \in \Img {T + I_U}$
Thus:
== Sources ==
* : Chapter $27$: Index Theory
Category:Fredholm Operators
Category:Vector Spaces
Category:Functional Analysis
Degree of Algebraic Curve/Examples/x y = 4

== Example of Degree of Algebraic Curve ==
The algebraic curve defined by the equation:
:$y^2 = 2 x$
is an example of an algebraic curve which has degree $2$.
That is, it is a quadratic curve.
== Sources ==
* 
* 
Category:Examples of Degrees of Algebraic Curves
Degree of Algebraic Curve/Examples/y^2 = 2 x

== Example of Degree of Algebraic Curve ==
The algebraic curve defined by the equation:
:$y^2 = 2 x$
is an example of an algebraic curve which has degree $2$.
That is, it is a quadratic curve.
== Sources ==
* 
* 
Category:Examples of Degrees of Algebraic Curves
Degree of Differential Equation/Examples/Second Degree Second Order

== Example of Degree of Differential Equation ==
The differential equation:
:$\paren {\dfrac {\d^2 y} {\d x^2} }^2 = k x$
is an example of an order $2$ ordinary differential equation of degree $2$.
== Sources ==
* 
* 
Category:Examples of Degree of Differential Equation
Degree of Element of Finite Field Extension divides Degree of Extension

== Theorem ==
Let $F$ be a field whose zero is $0$ and whose unity is $1$.
Let $K / F$ be a finite field extension of degree $n$.
Let $\alpha \in K$ be algebraic over $F$.
Then the degree of $\alpha$ is a divisor of $n$.
== Proof ==
Let $\alpha \in K$.
The dimension of $K / F$ considered as a vector space is $n$.
Let $S$ be the set defined as:
:$S := \set {1, \alpha, \alpha^2, \ldots, \alpha_n}$
We have that:
:$\card S = n + 1$
From Cardinality of Linearly Independent Set is No Greater than Dimension:
:$S$ is linearly dependent on $F$.
Hence there are scalars $c_0, c_1, \ldots, c_n \in F$, not all zero, such that:
:$c_0 + c_1 \alpha + c_2 \alpha^2 + \dotsb + c_n \alpha_n = 0$
which is a polynomial of degree $n$.
So $\alpha$ is algebraic over $F$ with degree no greater than $n$.
Consider $\map F \alpha$, the simple algebraic extension of $F$ on $\alpha$.
We have that:
:$F \subseteq \map F \alpha \subseteq K$
Let $\alpha$ be algebraic over $F$ with degree $m$.
Then $\map F \alpha$ is a finite extension of $F$ with degree $\index {\map F \alpha} F = m$.
We also have that $K$ is a finite extension of $F$ with degree $n$.
So by Degree of Field Extensions is Multiplicative:
:$\index K F = \index K {\map F \alpha} \index {\map F \alpha} F$
But $\index K F = n$ and $\index {\map F \alpha} F = m$
so it follows that:
:$m \divides n$
The result follows.
== Sources ==
* : Chapter $8$: Field Extensions: $\S 38$. Simple Algebraic Extensions: Theorem $74 \ \text {(i)}$
Category:Field Extensions
Degree of Field Extensions is Multiplicative

== Theorem ==
Let $E, K$ and $F$ be fields.
Let $E / K$ and $K / F$ be finite field extensions.
Then $E / F$ is a finite field extension, and:
:$\index E F = \index E K \index K F$
where $\index E F$ denotes the degree of $E / F$
== Proof ==
First, note that $E / F$ is a field extension as $F \subseteq K \subseteq E$.
Suppose that $\index E K = m$ and $\index K F = n$.
Let $\alpha = \set {a_1, \ldots, a_m}$ be a basis of $E / K$, and $\beta = \set {b_1, \ldots, b_n}$ be a basis of $K / F$.
We wish to prove that the set:
:$\gamma = \set {a_i b_j: 1 \le i \le m, 1 \le j \le n}$
is a basis of $E / F$.
As $\alpha$ is a basis of $E / K$, we have, for all $c \in E$:
:$\ds c = \sum_{i \mathop = 1}^m c_i a_i$, for some $c_i \in K$.
Define $\ds b := \sum_{j \mathop = 1}^n b_j$ and $d_i := \dfrac {c_i} b$.
Note $b \ne 0$ since $\beta$ is linearly independent over $F$, and $d_i \in K$ since $b, c_i \in K$.
Now we have:
:$\ds c = \sum_{i \mathop = 1}^m \frac {c_i} b \cdot b \cdot a_i = \sum_{i \mathop = 1}^m \sum_{j \mathop = 1}^n d_i a_i b_j$
Thus $\gamma$ is seen to be a spanning set of $E / F$.
To show $\gamma$ is linearly independent, suppose that for some $c_{i j} \in F$:
:$\ds \sum_{i \mathop = 1}^m \sum_{j \mathop = 1}^n c_{i j} a_i b_j = 0$
Then we have (as fields are commutative rings):
Hence $\gamma$ is a linearly independent spanning set; thus it is a basis.
Recalling the definition of $\gamma$ as $\set {a_i b_j: 1 \le i \le m, 1 \le j \le n}$, we have:
:$\size {\gamma} = m n = \index E K \index K F$
as was to be shown.
== Also known as ==
This result is also known as the degree equation, or the tower rule or tower law, from the definition of a tower of fields.
== Sources ==
* : Chapter $8$: Field Extensions: $\S 36$. The Degree of a Field Extension: Theorem $68$
Category:Field Extensions
Degree of Product of Polynomials over Integral Domain not Less than Degree of Factors

== Theorem ==
Let $\struct {R, +, \circ}$ be an integral domain whose zero is $0_R$.
Let $R \sqbrk X$ be the ring of polynomial forms over $R$ in the indeterminate $X$.
For $f \in R \sqbrk X$ let $\map \deg f$ be the degree of $f$.
Then if neither $f$ nor $g$ are the null polynomial:
:$\forall f, g \in R \sqbrk X: \map \deg {f g} \ge \map \deg f$
== Proof ==
From Degree of Product of Polynomials over Integral Domain, we have:
:$\map \deg {f g} = \map \deg f + \map \deg g$
But $\map \deg g \ge 0$ by definition of degree, as $g$ is not null.
Hence the result.
== Sources ==
* : Chapter $6$: Polynomials and Euclidean Rings: $\S 27$. Euclidean Rings: Theorem $51$
Category:Polynomial Theory
Degree of Product of Polynomials over Ring

== Theorem ==
Let $\struct {R, +, \circ}$ be a commutative ring with unity whose zero is $0_R$.
Let $R \sqbrk X$ be the polynomial ring over $R$ in the indeterminate $X$.
Let $f, g \in R \sqbrk X$.
Then:
:$\forall f, g \in R \sqbrk X: \map \deg {f g} \le \map \deg f + \map \deg g$
where:
:$\map \deg f$ denotes the degree of $f$.
=== Corollary 1 ===
=== Corollary 2 ===
== Proof ==
Let the leading coefficient of:
:$\map f X$ be $a_n$
:$\map g X$ be $b_n$.
Then:
Consider the leading coefficient of the product $\map f X \map g X$: call it $c$.
From the definition of polynomial addition and polynomial multiplication: 
:$\map f X \map g X = c X^{n + m} + \cdots + a_0 b_0$
Clearly the highest term of $\map f X \map g X$ can have an index no higher than $n + m$.
Hence the result:
:$\map \deg {f g} \not > \map \deg f + \map \deg g$
Next, note that the general ring with unity $\struct {R, +, \circ}$ may have proper zero divisors.
Therefore it is possible that $X^{n + m}$ may equal $0_R$.
If that is the case, then the highest term will have an index definitely less than $n + m$.
That is, in that particular case:
:$\map \deg {f g} < \map \deg f + \map \deg g$
Thus, for a general ring with unity $\struct {R, +, \circ}$:
:$\map \deg {f g} \le \map \deg f + \map \deg g$
== Also see ==
* Degree of Sum of Polynomials
== Sources ==
* : $\S 3.2$: Polynomial rings: Lemma $3.7 \ \text{(ii)}$ 
Category:Polynomial Theory
Category:Degree of Product of Polynomials over Ring
Degree of Product of Polynomials over Ring/Corollary 1

== Corollary to Degree of Product of Polynomials over Ring ==
Let $\struct {R, +, \circ}$ be a ring with unity whose zero is $0_R$.
Let $R \sqbrk X$ be the ring of polynomials over $R$ in the indeterminate $X$.
For $f \in R \sqbrk X$ let $\deg f$ be the degree of $f$.
Let $R$ have no proper zero divisors.
Then:
:$\forall f, g \in R \sqbrk X: \map \deg {f g} = \deg f + \deg g$
== Proof ==
Let the leading coefficient of:
:$\map f X$ be $a_n$
:$\map g X$ be $b_m$.
From Degree of Product of Polynomials over Ring:
:$\map \deg {f g} \le \deg f + \deg g$
From the definition of polynomial multiplication:
:$\map f X \map g X = a_n b_m X^{n + m} + \cdots + a_0 b_0$
As $\struct {R, +, \circ}$ has no proper zero divisors the $X^{n + m}$ term can not equal $0_R$ and so:
:$\map \deg {f g} = \deg f + \deg g$
Category:Degree of Product of Polynomials over Ring