avewright/proofwiki-math huggingface dataset:
Theorem: Scaled Sine Functions of Integer Multiples form Orthonormal Set

For all $n \in \Z_{>0}$, let $\map {\phi_n} x$ be the real function defined on the interval $\openint 0 \lambda$ as:
:$\map {\phi_n} x = \sqrt {\dfrac 2 \lambda} \sin \dfrac {n \pi x} \lambda$
Let $S$ be the set:
:$S = \set {\phi_n: n \in \Z_{>0} }$
Then $S$ is an orthonormal set.

Proof:
Consider the definite integral:
:$I_{m n} = \ds \int_0^\lambda \map {\phi_m} x \map {\phi_n} x \rd x$
From Sine Function is Odd, each of $\map {\phi_n} x$ is an odd function.
From Odd Function Times Odd Function is Even, $\map {\phi_m} x \map {\phi_n} x$ is even.
That is:
:$\paren {\sqrt {\dfrac 2 \lambda} \sin \dfrac {m \pi x} \lambda} \paren {\sqrt {\dfrac 2 \lambda} \sin \dfrac {n \pi x} \lambda}$
is an even function.
Let $u = \dfrac {\pi x} \lambda$.
We have:
{{begin-eqn}}
{{eqn | l = \dfrac {\d u} {\d x}
      | r = \dfrac \pi \lambda
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d x} {\d u}
      | r = \dfrac \lambda \pi
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = x
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u
      | r = \dfrac {\pi \times 0} \lambda
      | c = 
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = x
      | r = \lambda
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u
      | r = \dfrac {\pi \times \lambda} \lambda
      | c = 
}}
{{eqn | r = \pi
      | c = 
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = I_{m n}
      | r = \int_0^\lambda \map {\phi_m} x \map {\phi_n} x \rd x
      | c = 
}}
{{eqn | r = \int_0^\lambda \paren {\sqrt {\dfrac 2 \lambda} \sin \frac {m \pi x} \lambda} \paren {\sqrt {\dfrac 2 \lambda} \sin \frac {n \pi x} \lambda} \rd x
      | c = 
}}
{{eqn | r = \frac 2 \lambda \int_0^\lambda \sin \frac {m \pi x} \lambda \sin \frac {n \pi x} \lambda \rd x
      | c = Linear Combination of Definite Integrals
}}
{{eqn | r = \frac 2 \lambda \int_0^\pi \frac \lambda \pi \sin m u \sin n u \rd u
      | c = Integration by Substitution
}}
{{eqn | r = \frac 2 \lambda \frac \lambda \pi \int_0^\pi \sin m u \sin n u \rd u
      | c = Linear Combination of Definite Integrals
}}
{{eqn | r = \frac 2 \pi \int_0^\pi \sin m u \sin n u \rd u
      | c = 
}}
{{eqn | r = \frac 1 \pi \int_{-\pi}^\pi \sin m u \sin n u \rd u
      | c = Definite Integral of Even Function
}}
{{eqn | r = \frac 1 \pi \pi \delta_{m n}
      | c = Integral over $2 \pi$ of $\sin m u \sin n u$
}}
{{eqn | r = \delta_{m n}
      | c = 
}}
{{end-eqn}}
Hence the result by definition of orthonormal set.
{{qed}}
Theorem: Correspondence Theorem for Quotient Rings/Bijection

The direct image mapping $\pi^\to$ and the inverse image mapping $\pi^\gets$ induce reverse bijections between the ideals of $A$ containing $\mathfrak a$ and the ideals of $A/\mathfrak a$, specifically:
Let $I$ be the set of ideals of $A$ containing $\mathfrak a$.
Let $J$ be the set of ideals of $A / \mathfrak a$.
Then:
:$(1): \quad$ For every ideal $\mathfrak b \in I$, its image $\map {\pi^\to} {\mathfrak b} = \map \pi {\mathfrak b} \in J$
:$(2): \quad$ For every ideal $\mathfrak c \in J$, its preimage $\map {\pi^\gets} {\mathfrak c} = \map {\pi^{-1} } {\mathfrak c} \in I$
:$(3): \quad$ The restrictions $\pi^\to: I \to J$ and $\pi^\gets: J \to I$ are reverse bijections.

Proof:
Follows from Correspondence Theorem for Ring Epimorphisms/Bijection
{{qed}}
Category:Quotient Rings
0snouo05fh0g4n0ggttzc3fcfc09bmb
Theorem: Correspondence Theorem for Ring Epimorphisms/Bijection

The direct image mapping $\pi^\to$ and the inverse image mapping $\pi^\gets$ induce reverse bijections between $I$ and $J$, specifically:
#For every ideal $\mathfrak a \in I$, its image $\pi^{\to}(\mathfrak a) = \pi(\mathfrak a) \in J$.
#For every ideal $\mathfrak b \in J$, its preimage $\pi^{\gets}(\mathfrak b) = \pi^{-1}(\mathfrak b) \in I$.
#The restrictions $\pi^\to : I \to J$ and $\pi^\gets : J \to I$ are reverse bijections.

Proof:
The first statements follow from:
* Preimage of Ideal under Ring Homomorphism is Ideal
* Image of Ideal under Ring Epimorphism is Ideal
The last statement follows from:
* Image of Preimage of Ideal under Ring Epimorphism
* Preimage of Image of Ideal under Ring Homomorphism
{{qed}}
Category:Ring Homomorphisms
6brohngslt7sxuhimqju0i9m8a0acx8
Theorem: Image of Ideal under Ring Epimorphism is Ideal

Let $f : A \to B$ be a ring epimorphism.
Let $I \subseteq A$ be an ideal.
Then its image $f(I) \subseteq B$ is an ideal.

Proof:
{{proof wanted}}
Category:Ring Homomorphisms
k1fwp02uwn3fgkog4t5wmwpm3xykfze
Theorem: Preimage of Prime Ideal under Ring Homomorphism is Prime Ideal

Let $A$ and $B$ be commutative rings with unity.
Let $f : A \to B$ be a ring homomorphism.
Let $\mathfrak p \subseteq B$ be a prime ideal.
Then its preimage $\map {f^{-1} } {\mathfrak p}$ is a prime ideal of $A$.

Proof:
By Preimage of Ideal under Ring Homomorphism is Ideal, $\map {f^{-1} } {\mathfrak p}$ is a ideal of $A$.
Let $B / \mathfrak p$ be the quotient ring.
By Prime Ideal iff Quotient Ring is Integral Domain, $B / \mathfrak p$ is an integral domain.
By Quotient Ring of Kernel of Ring Epimorphism, the quotient ring epimorphism $B \to B / \mathfrak p$ has kernel $\mathfrak p$.
By Kernel of Composition of Ring Homomorphisms, the composition $A \overset f \to B \to B / \mathfrak p$ has kernel $\map {f^{-1} } {\mathfrak p}$.
By Universal Property of Quotient Ring, there exists a ring homomorphism $A / \map {f^{-1} } {\mathfrak p} \to B / \mathfrak p$.
{{link wanted|a theorem why it is injective}}.
By Subring of Integral Domain is Integral Domain, $A / \map {f^{-1} } {\mathfrak p}$ is an integral domain.
By Prime Ideal iff Quotient Ring is Integral Domain, $\map {f^{-1} } {\mathfrak p}$ is a prime ideal of $A$.
{{qed}}
Theorem: Integral Domain iff Zero Ideal is Prime

Let $A$ be a commutative ring with unity.
{{TFAE}}
:$(1): \quad A$ is an integral domain
:$(2): \quad$ the zero ideal $\ideal 0 \subseteq A$ is prime

Proof:
By Prime Ideal iff Quotient Ring is Integral Domain, $\ideal 0$ is prime {{iff}} the quotient ring $A / \ideal 0$ is an integral domain.
By Quotient Ring by Null Ideal, $A \cong A / \ideal 0$.
{{qed}}
Category:Integral Domains
Category:Prime Ideals of Rings
47fvl892omw913l26myb2x9f28eq91b
Theorem: Kernel of Composition of Ring Homomorphisms

Let $f : A \to B$ and $g : B \to C$ be ring homomorphisms.
Let $g \circ f$ be their composition.
Then the kernel of $g \circ f$ is the preimage under $f$ of the kernel of $g$:
:$\map \ker {g \circ f} = f^{-1} \sqbrk {\ker g}$

Proof:
By definition, the kernel of a ring homomorphism is its kernel when considered as a group homomorphism between the additive groups.
The result follows from Kernel of Composition of Group Homomorphisms.
{{qed}}
Category:Ring Homomorphisms
sdjqic2fcbk30acpe13xsgurfciujpe
Theorem: Ring Epimorphism Preserves Unity

Let $A$ be a ring with unity $1$.
Let $B$ be a ring.
Let $f: A \to B$ be a ring epimorphism.
Then $\map f 1$ is a unity of $B$.

Proof:
By definition, $f$ is a semigroup homomorphism between multiplicative semigroups.
A unity of a ring is by definition an identity element of its multiplicative semigroup.
Thus the result follows from Epimorphism Preserves Identity.
{{qed}}
Category:Ring Epimorphisms
9nofbcnttzpsssgf79g3ug472j6fwcu
Theorem: Complement of Prime Ideal of Ring is Multiplicatively Closed

Let $R$ be a commutative ring with unity.
Let $P \subset R$ be a prime ideal of $R$.
Then its complement $R \setminus P$ is multiplicatively closed.

Proof:
Since $P$ is a proper ideal by {{Defof|Prime Ideal of Commutative and Unitary Ring|Prime Ideal}}, we have:
:$1_R \in R \setminus P$
where $1_R$ is the unity of $R$.
{{AimForCont}} $R \setminus P$ is not multiplicatively closed.
That is:
:$\exists a, b \in R \setminus P: a b \notin R \setminus P$
This means:
:$a b \in P$
This contradicts the assertion that $P$ is a prime ideal of $R$.
{{qed}}
Theorem: Derivative of Gamma Function

:$\ds \map {\Gamma'} x = \int_0^\infty t^{x - 1} \ln t \, e^{-t} \rd t$
where $\map {\Gamma'} x$ denotes the derivative of the Gamma function evaluated at $x$.

Proof:
{{begin-eqn}}
{{eqn	| l = \map {\Gamma'} x
	| r = \frac \d {\d x} \int_0^\infty t^{x - 1} e^{-t} \rd t
	| c = {{Defof|Gamma Function}}
}}
{{eqn	| r = \int_0^\infty \frac {\partial} {\partial x} t^{x - 1} e^{-t} \rd t
	| c = Leibniz's Integral Rule
}}
{{eqn	| r = \int_0^\infty t^{x-1} \ln t \, e^{-t} \rd t
	| c = Derivative of Power of Constant
}}
{{end-eqn}}
{{qed}}
Category:Gamma Function
Category:Derivatives
ablqijf045xngqhhekk2ydxlbe72yhi
Theorem: Derivative of Gamma Function

:$\ds \map {\Gamma'} x = \int_0^\infty t^{x - 1} \ln t \, e^{-t} \rd t$
where $\map {\Gamma'} x$ denotes the derivative of the Gamma function evaluated at $x$.

Proof:
From Reciprocal times Derivative of Gamma Function:
:$\ds \dfrac {\map {\Gamma'} z} {\map \Gamma z} = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {z + n - 1} }$
Setting $z = 1$:
{{begin-eqn}}
{{eqn | l = \frac {\map {\Gamma'} 1} {\map \Gamma 1}
      | r = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {1 + n - 1} }
      | c = 
}}
{{eqn | r = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 n}
      | c = 
}}
{{eqn | r = -\gamma + 0
      | c = 
}}
{{eqn | r = -\gamma
      | c = 
}}
{{end-eqn}}
Using Gamma Function Extends Factorial:
:$\map \Gamma 1 = \paren {1 - 1}! = 1$
Hence:
:$\map {\Gamma'} 1 = -\gamma \map \Gamma 1 = -\gamma$
{{qed}}
Theorem: Derivative of Gamma Function

:$\ds \map {\Gamma'} x = \int_0^\infty t^{x - 1} \ln t \, e^{-t} \rd t$
where $\map {\Gamma'} x$ denotes the derivative of the Gamma function evaluated at $x$.

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {\map \Gamma z}
      | r = z e^{\gamma z} \prod_{n \mathop = 1}^\infty \paren {\paren {1 + \frac z n} e^{-z / n} }
      | c = Weierstrass Form of Gamma Function
}}
{{eqn | ll= \leadsto
      | l = \map \Gamma z
      | r = \frac {e^{-\gamma z} } z \prod_{n \mathop = 1}^\infty \frac {e^{z/n} } {1 + \frac z n}
      | c = reciprocal of both sides
}}
{{eqn | ll= \leadsto
      | l = \map {\Gamma'} z
      | r = \map {\dfrac \d {\d z} } {\frac {e^{-\gamma z} } z \prod_{n \mathop = 1}^\infty \frac {e^{z/n} } {1 + \frac z n} }
      | c = differentiating {{WRT|Differentiation}} $z$
}}
{{eqn | ll= \leadsto
      | l = \map {\Gamma'} z
      | r = -\frac {e^{-\gamma z} \paren {1 + \gamma z} } {z^2} \prod_{n \mathop = 1}^\infty \paren {\frac {e^{z / n} } {\paren {1 + \frac z n} } } + \frac {e^{-\gamma z} } z \sum_{n \mathop = 1}^\infty \paren {\frac z {n \paren {z + n} } \prod_{i \mathop = 1}^\infty \frac {e^{z / i} } {1 + \frac z i} }
      | c = Product Rule for Derivatives
}}
{{eqn | r = -\frac {e^{-\gamma z} \paren {1 + \gamma z} } {z^2} \frac z {e^{-\gamma z} } \map \Gamma z + \frac {e^{-\gamma z} } z \sum_{n \mathop = 1}^\infty \paren {\frac z {n \paren {z + n} } \frac z {e^{-\gamma z} } \map \Gamma z}
      | c = simplifying the continued product
}}
{{eqn | r = -\frac {1 + \gamma z} z \map \Gamma z + \sum_{n \mathop = 1}^\infty \paren {\frac {z \map \Gamma z} {n \paren {z + n} } }
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac {\map {\Gamma'} z} {\map \Gamma z}
      | r = -\frac {1 + \gamma z} z + \sum_{n \mathop = 1}^\infty \paren {\frac z {n \paren {z + n} } }
      | c = dividing both sides by $\map \Gamma z$
}}
{{eqn | r = -\gamma - \frac 1 z + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {z + n} }
}}
{{eqn | r = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {z + n - 1} }
      | c = rearranging the series
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Gamma Function

:$\ds \map {\Gamma'} x = \int_0^\infty t^{x - 1} \ln t \, e^{-t} \rd t$
where $\map {\Gamma'} x$ denotes the derivative of the Gamma function evaluated at $x$.

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {\map \Gamma z}
      | r = z e^{\gamma z} \prod_{n \mathop = 1}^\infty \paren {\paren {1 + \frac z n} e^{-z / n} }
      | c = Weierstrass Form of Gamma Function
}}
{{eqn | ll= \leadsto
      | l = \map \Gamma z
      | r = \frac {e^{-\gamma z} } z \prod_{n \mathop = 1}^\infty \frac {e^{z/n} } {1 + \frac z n}
      | c = reciprocal of both sides
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\map {\Gamma} z}
      | r = \map \ln {\frac {e^{-\gamma z} } z \prod_{n \mathop = 1}^\infty \frac {e^{z/n} } {1 + \frac z n} }
      | c = logarithm of both sides
}}
{{eqn | r = \map \ln {e^{-\gamma z} } - \ln z + \sum_{n \mathop = 1}^\infty \paren { \map \ln {e^{z/n} } -  \map \ln {1 + \frac z n} }
      | c = Sum of Logarithms and Difference of Logarithms
}}
{{eqn | r = -\gamma z \ln e - \ln z + \sum_{n \mathop = 1}^\infty \paren {\frac z n \ln e -  \map \ln {1 + \frac z n} }
      | c = Logarithm of Power
}}
{{eqn | r = -\gamma z - \ln z + \sum_{n \mathop = 1}^\infty \paren {\frac z n - \map \ln {1 + \frac z n} }
      | c = Natural Logarithm of e is 1
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d z} } {\map \ln {\map {\Gamma} z} }
      | r = \map {\dfrac \d {\d z} } {-\gamma z - \ln z + \sum_{n \mathop = 1}^\infty \paren {\frac z n - \map \ln {1 + \frac z n} } }
      | c = differentiating {{WRT|Differentiation}} $z$
}}
{{eqn | ll= \leadsto
      | l = \frac {\map {\Gamma'} z} {\map \Gamma z}
      | r = -\gamma - \frac 1 z + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac {\frac 1 n} {1 + \frac z n} }
      | c = Derivative of Composite Function and Derivative of Natural Logarithm Function
}}
{{eqn | r = -\gamma - \frac 1 z + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {z + n} }
}}
{{eqn | r = -\gamma - \frac 1 z + \paren {\paren {\frac 1 1 - \frac 1 {z + 1} } + \paren {\frac 1 2 - \frac 1 {z + 2} } + \paren {\frac 1 3 - \frac 1 {z + 3} } + \cdots}
}}
{{eqn | r = -\gamma + \paren {\paren {\frac 1 1 - \frac 1 z } + \paren {\frac 1 2 - \frac 1 {z + 1} } + \paren {\frac 1 3 - \frac 1 {z + 2} } + \cdots}
      | c = shifting the terms with $z$ one to the right
}}
{{eqn | r = -\gamma + \sum_{n \mathop = 1}^\infty \paren {\frac 1 n - \frac 1 {z + n - 1} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Hankel Representation of Riemann Zeta Function

Let $C$ be the Hankel contour.
Then for $s \in \C \setminus \Z_{>0}$: 
:$\ds \map \zeta s = \frac {i \Gamma \paren {1 - s} } {2 \pi} \oint_C \frac {\paren {-z}^{s - 1} } {e^z - 1} \rd z$
where:
:$\zeta$ is the Riemann Zeta function
:$\Gamma$ is the Gamma function.

Proof:
{{ProofWanted}}
{{Namedfor|Hermann Hankel|cat = Hankel}}
Theorem: Argument Principle

Let $\gamma$ be a closed contour.
Let $D$ be the region enclosed by $\gamma$. 
Let $f$ be a function meromorphic on $D$. 
Let $f$ be holomorphic with no zeroes on $\gamma$.
Let $N$ denote the number of zeroes of $f$ in $D$, counted up to multiplicity.
Let $P$ denote the number of poles of $f$ in $D$, counted up to order.
{{explain|order}}
Then:
:$\ds N - P = \frac 1 {2\pi i} \oint_\gamma \frac {\map {f'} z} {\map f z} \rd z$

Proof:
Let $n_1, n_2, n_3 \ldots n_N$ denote the zeroes of $f$, and $p_1, p_2, p_3 \ldots p_P$ denote its poles. 
Then, there exists a non-zero holomorphic function $g$ such that:
:$\ds \map f x = \frac {\prod_{k \mathop = 1}^N \paren {z - n_k} } {\prod_{j \mathop = 1}^P \paren {z - p_j} } \map g z$
Taking the logarithmic derivative:
{{begin-eqn}}
{{eqn	| l = \map \LL {\map f z}
	| r = \frac {\map {f'} z} {\map f z}
	| c = {{Defof|Logarithmic Differentiation}}
}}
{{eqn	| r = \map \LL {\prod_{k \mathop = 1}^N \paren {z - n_k} } - \map \LL {\prod_{j \mathop = 1}^P \paren {z - p_j} } + \map \LL {\map g z}
}}
{{eqn	| r = \sum_{k \mathop = 1}^N \frac 1 {z - n_k} - \sum_{j \mathop = 1}^P \frac 1 {z - p_j} + \frac {\map {g'} z} {\map g z} 
}}
{{end-eqn}}
Then: 
{{begin-eqn}}
{{eqn	| l = \oint_\gamma \frac {\map {f'} z} {\map f z} \rd z
	| r = \oint_\gamma \paren {\sum_{k \mathop = 1}^N \frac 1 {z - n_k} - \sum_{j \mathop = 1}^P \frac 1 {z - p_j} + \frac {\map {g'} z} {\map g z} } \rd z
}}
{{eqn	| r = \sum_{k \mathop = 1}^N \oint_\gamma \frac 1 {z - n_k} \rd z - \sum_{j \mathop = 1}^P \oint_\gamma \frac 1 {z - p_j} \rd z + \oint_\gamma \frac {\map {g'} z} {\map g z} \rd z 
	| c = Linear Combination of Contour Integrals
}}
{{eqn	| r = \sum_{k \mathop = 1}^N 2 \pi i - \sum_{j \mathop = 1}^P 2 \pi i + \oint_\gamma \frac {\map {g'} z} {\map g z} \rd z
}}
{{eqn	| r = 2\pi i \paren {N - P} + \oint_\gamma \frac {\map {g'} z} {\map g z} \rd z
}}
{{end-eqn}}
By our construction of $g$, $\dfrac {g'} g$ is holomorphic on $D$ so, by the Cauchy Integral Theorem, the integral is equal to zero.
We therefore have:
:$\ds \oint_\gamma \frac {\map {f'} z} {\map f z} \rd z = 2\pi i \paren {N - P}$
Hence:
:$\ds N - P = \frac 1 {2\pi i} \oint_\gamma \frac {\map {f'} z} {\map f z} \rd z$
{{qed}}
Category:Complex Analysis
Category:Named Theorems
6m1yjdqth0nimst97pkelifmolg1ump
Theorem: Ring with Unity has Prime Ideal

Let $A$ be a non-trivial commutative ring with unity.
Then $A$ has a prime ideal.

Proof:
By Krull's Theorem, $A$ has a maximal ideal.
By Maximal Ideal of Commutative and Unitary Ring is Prime Ideal, $A$ has a prime ideal.
{{qed}}
Theorem: Proper Ideal of Ring is Contained in Maximal Ideal

Let $A$ be a commutative ring with unity.
Let $\mathfrak a \subseteq A$ be a proper ideal.
Then there exists a maximal ideal $\mathfrak m$ with $\mathfrak a \subseteq \mathfrak m$.

Proof:
Let $A / \mathfrak a$ be the quotient ring.
By Proper Ideal iff Quotient Ring is Non-Null, $A / \mathfrak a$ is non-null.
By Krull's Theorem, $A / \mathfrak a$ has a maximal ideal.
By Correspondence Theorem for Quotient Rings, $A$ has a maximal ideal containing $\mathfrak a$.
{{qed}}
Category:Commutative Algebra
Category:Maximal Ideals of Rings
ltig1lv211aie8k6tzek5i2weo5uol5
Theorem: Proper Ideal iff Quotient Ring is Non-Null

Let $A$ be a commutative ring.
Let $\mathfrak a \subseteq A$ be an ideal.
{{TFAE}}
:$(1): \quad \mathfrak a$ is a proper ideal of $A$.
:$(2): \quad$ The quotient ring $A / \mathfrak a$ is a non-null ring.

Proof:
=== 1 implies 2 ===
Suppose $\mathfrak a$ is a proper ideal of $A$.
That is:
:$\exists x \in A \setminus \mathfrak a$
By definition of congruence modulo subgroup:
:$x + \mathfrak a \ne 0 + \mathfrak a$
in the quotient ring $A / \mathfrak a$.
Hence $A / \mathfrak a$ is a non-null ring.
{{qed|lemma}}
Theorem: Residue of Quotient

Let $f$ and $g$ be functions holomorphic on some region containing $a$. 
Let $g$ have a zero of multiplicity $1$ at $a$. 
Then:
:$\Res {\dfrac f g} a = \dfrac {\map f a} {\map {g'} a}$
{{explain|definition of "Res", by a link to Residue}}

Proof:
As $g$ has a zero of multiplicity $1$ at $a$, $\dfrac f g$ has a simple pole at $a$ by definition.
So: 
{{begin-eqn}}
{{eqn	| l = \Res {\dfrac f g} a
	| r = \lim_{z \mathop \to a} \paren {z - a} \frac {\map f z} {\map g z}
	| c = Residue at Simple Pole
}}
{{eqn	| r = \lim_{z \mathop \to a} \frac {\map f z} {\frac {\map g z - \map g a} {z - a} }
	| c = $\map g a = 0$
}}
{{eqn	| r = \frac {\lim_{z \mathop \to a} \map f z} {\lim_{z \mathop \to a} \frac {\map g z - \map g a} {z - a} } 
	| c = Quotient Rule for Limits of Complex Functions
}}
{{eqn	| r = \frac {\map f a} {\map {g'} a}
	| c = {{Defof|Derivative of Complex Function}}
}} 
{{end-eqn}}
{{qed}}
Category:Complex Analysis
hvunijteq2bh3nbmorrwiqx9ie3tj5b
Theorem: Holomorphic Function is Analytic

Let $a \in \C$ be a complex number.
Let $r > 0$ be a real number.
Let $f$ be a function holomorphic on some open disk $D = \map B {a, r}$. 
Then $f$ is complex analytic on $D$.

Proof:
Let $z \in D$.
Then: 
{{begin-eqn}}
{{eqn | l = \map f z
      | r = \frac 1 {2 \pi i} \oint_{\partial D} \frac {\map f t} {t - z} \rd t
      | c = Cauchy's Integral Formula
}}
{{eqn | r = \frac 1 {2 \pi i} \oint_{\partial D} \frac {\map f t} {\paren {t - a} \paren {1 - \frac {z - a} {t - a} } } \rd t
}}
{{end-eqn}}
Note that for all $t \in \partial D$, we have:
:$\cmod {z - a} < \cmod {t - a} = r$.
Therefore:
:$\cmod {\dfrac {z - a} {t - a} } < 1$
so Sum of Infinite Geometric Sequence may be applied.
This gives:
{{begin-eqn}}
{{eqn | l = \map f z
      | r = \frac 1 {2 \pi i} \oint_{\partial D} \frac {\map f t} {t - a} \sum_{n \mathop = 0}^\infty \paren {\frac {z - a} {t - a} }^n \rd t
}}
{{eqn | r = \frac 1 {2 \pi i} \oint_{\partial D} \sum_{n \mathop = 0}^\infty \map f t \frac {\paren {z - a}^n} {\paren {t - a}^{n + 1} } \rd t
}}
{{end-eqn}}
From Continuous Function on Compact Space is Bounded, there exists a real $M \ge 0$, such that:
:$\forall t \in \partial D: \cmod {\map f t} \le M$
As $\cmod {\dfrac {z - a} {t - a} } < 1$, there exists a real $0 \le N < 1$ such that:
:$\cmod {\dfrac {z - a} {t - a} } \le N$
Then: 
:$\cmod {\dfrac {\paren {z - a}^n} {\paren {t - a}^{n + 1} } \map f t} = \cmod {\dfrac 1 {t - a} } \cmod {\dfrac {\paren {z - a}^n} {\paren {t - a}^n} } \cmod {\map f t} \le \dfrac 1 r M N^n$ 
As $N < 1$, we have that $\ds \frac 1 r \sum_{n \mathop = 0}^\infty M N^n$ converges by Sum of Infinite Geometric Sequence. 
Therefore by the Weierstrass M-Test, we have that: 
:$\ds \sum_{n \mathop = 0}^\infty \map f t \frac {\paren {z - a}^n} {\paren {t - a}^{n + 1} }$ 
converges uniformly on $D$.
Therefore: 
:$\ds \frac 1 {2 \pi i} \oint_{\partial D} \sum_{n \mathop = 0}^\infty \map f t \frac {\paren {z - a}^n} {\paren {t - a}^{n + 1} } \rd t = \sum_{n \mathop = 0}^\infty \paren {z - a}^n \paren {\frac 1 {2 \pi i} \oint_{\partial D} \frac {\map f t} {\paren {t - a}^{n + 1} } \rd t}$
Let: 
:$\ds c_n = \frac 1 {2 \pi i} \oint_{\partial D} \frac {\map f t} {\paren {t - a}^{n + 1} } \rd t$
Then: 
:$\ds \map f z = \sum_{n \mathop = 0}^\infty c_n \paren {z - a}^n$ 
so $f$ is complex analytic on $D$. 
{{qed}}
Theorem: Schwarz's Lemma

Let $D$ be the unit disk centred at $0$.
Let $f: D \to \C$ be a holomorphic function.
Let $\map f 0 = 0$ and $\cmod {\map f z} \le 1$ for all $z \in D$. 
Then $\cmod {\map {f'} 0} \le 1$, and $\cmod {\map f z} \le \cmod z$ for all $z \in D$.

Proof:
=== Lemma ===
{{:Schwarz's Lemma/Lemma}}{{qed|lemma}}
Let $g: D \to \C$ be a complex function such that:
:$\map g z = \begin {cases} \dfrac {\map f z} z & z \ne 0 \\ \map {f'} 0 & z = 0 \end {cases}$
By the {{Lemma|Schwarz's Lemma}}, $g$ is holomorphic on $D$. 
Let $r$ be a real number with $0 < r < 1$. 
Let $C_r$ be the closed disk of radius $r$ centered at $0$.
Since $C_r$ is compact, by Continuous Function on Compact Space is Bounded, $\cmod g$ attains its maximum on $C_r$.
Let $\alpha \in C_r$ be a point where this maximum is attained.
If $g$ is constant, then we can pick $\alpha$ to be any point on $C_r$. 
If $g$ is non-constant, then by the Maximum Modulus Principle, $\alpha$ necessarily lies on the boundary of $C_r$.
That is, $\cmod \alpha = r$ if $g$ is non-constant. 
If $g$ is constant, pick $\alpha$ such that $\cmod \alpha = r$ to avoid splitting into cases.
With that, for all $z \in C_r$ we have:
:$\cmod {\map g z} \le \cmod {\map g \alpha}$
Since $0$ lies in the interior of $C_r$, we must have $\alpha \ne 0$, so:
{{begin-eqn}}
{{eqn | l = \cmod {\map g \alpha}
      | r = \cmod {\frac {\map f \alpha} \alpha}
}}
{{eqn | r = \frac {\cmod {\map f \alpha} } {\cmod \alpha}
}}
{{eqn | o = \le
      | r = \frac 1 r
      | c = since $\cmod {\map f z} \le 1$ on $D$, and $\cmod \alpha = r$
}}
{{end-eqn}}
So, for all $z \in C_r$ we have: 
:$\cmod {\map g z} \le \dfrac 1 r$
{{AimForCont}} there exists $\omega \in D$ with: 
:$\cmod \omega < 1$
:$\cmod {\map g \omega} = 1 + \varepsilon > 1$
Note that we then have: 
:$0 < \dfrac 1 {1 + \varepsilon} < 1$
Note that on $C_R$ with $R > \map \max {\dfrac 1 {1 + \varepsilon}, \cmod \omega}$, we should have: 
:$\cmod {\map g z} \le \dfrac 1 R < 1 + \varepsilon$
However, we have $\omega \in C_R$ and: 
:$\cmod {\map g \omega} = 1 + \varepsilon$
a contradiction. 
So, it must be the case that: 
:$\cmod {\map g z} \le 1$
for all $z \in D$.
We have: 
:$\cmod {\map {f'} 0} = \cmod {\map g 0} \le 1$
Note that: 
:$\cmod {\map f 0} = 0$
so certainly: 
:$\cmod {\map f z} \le \cmod z$
for $z = 0$. 
Take $z \in D \setminus \set 0$, from: 
:$\cmod {\map g z} \le 1$
we have: 
:$\cmod {\dfrac {\map f z} z} \le 1$
that is: 
:$\cmod {\map f z} \le \cmod z$
hence the result.
{{qed}}
{{Namedfor|Karl Hermann Amandus Schwarz|cat = Schwarz}}
Category:Schwarz's Lemma
Category:Complex Analysis
itmdgesdsae03vfoe2wvtzquhzypaao