avewright/proofwiki-math huggingface dataset:
Theorem: Three Regular Tessellations/Hexagons

Regular hexagons form a regular tessellation:
:400px

Proof:
Let $s \in \R_{>0}$ be the side length of the regular hexagons.
For all $x, y \in \Z$, let the center $Q_{x,y}$ of each regular hexagon have Cartesian coordinates:
:$Q_{x,y} = s \tuple {x, \sqrt 3 y + \dfrac {\sqrt 3 \paren {3 - m} } 4}$
where:
:$m = \begin{cases} 1 & : \textrm {for $x$ even} \\ -1 & : \textrm{for $x$ odd} \end{cases}$
From Regular Hexagon is composed of Equilateral Triangles, it follows that each hexagon can be triangulated into six congruent equilateral triangles.
Also, each of the six equilateral triangles has side length $s$, and $Q_{x,y}$ as one of its vertices.
By Three Regular Tessellations:Triangles, there exists a regular tessellation of equilateral triangles with side length s.
Set:
:$i := 3 x$
:$j := 2 y + \dfrac {1-m} 2$
The hexagon center $Q_{x,y}$ corresponds to the six vertices:
:$A_{i+1, j}, A_{i+1, j+1}, B_{i-1,j}, B_{i-1,j+1}, C_{i,j}, C_{i,j+1} $
as they are labelled in the proof of Three Regular Tessellations:Triangles.
The six triangles in the triangulation of the hexagon correspond to the triangles of the regular tessellation:
:$\triangle A_{i+1, j} B_{i+1, j} C_{i+1, j}$
:$\triangle A_{i+1, j+1} B_{i+1, j+1} C_{i+1, j+1} $
:$\triangle A_{i-1, j} B_{i-1, j} C_{i-1, j} $
:$\triangle A_{i-1, j+1} B_{i-1, j+1} C_{i-1, j+1} $
:$\triangle A_{i, j} B_{i, j} C_{i, j}$
:$\triangle A_{i, j+1} B_{i, j+1} C_{i, j+1} $
as they are labelled in the proof of Three Regular Tessellations:Triangles.
For all $x' \in \Z$, there exist exactly one $x \in \Z$ and one $k \in \set {-1, 0, 1}$ such that:
:$x' = 3 x + k$
For all $y' \in \Z$, there exist exactly one $y \in \Z$ and one $k \in \set {0, 1}$ such that:
:$y' = 2 y + k$
which shows that each $\triangle A_{x', y'} B_{x', y'} C_{x', y'}$ is part of exactly one of the hexagons.
As the triangles form a regular tessellation of the plane, it follows that the hexagons also form a regular tessellation of the plane.
{{qed}}
Theorem: Finite Subset Bounds Element of Finite Suprema Set and Lower Closure

Let $L = \struct {S, \vee, \preceq}$ be join semilattice.
Let $I$ be ideal in $L$.
Let $X$ be non empty finite subset of $S$.
Let $x \in S$ such that
:$x \in \paren {\map {\operatorname {finsups} } {F \cup X} }^\preceq$
where
:$\operatorname {finsups}$ denotes the finite suprema set
:$X^\preceq$ denotes the lower closure of $X$.
Then there exists $a \in S$: $a \in I \land x \preceq a \vee \sup X$

Proof:
This follows by {{mutatis}} of the proof of Finite Subset Bounds Element of Finite Infima Set and Upper Closure.
{{qed}}
Theorem: Fermat Quotient of 2 wrt p is Square iff p is 3 or 7

Let $p$ be a prime number.
The Fermat quotient of $2$ with respect to $p$:
:$\map {q_p} 2 = \dfrac {2^{p - 1} - 1} p$
is a square {{iff}} $p = 3$ or $p = 7$.

Proof:
When $p = 3$:
:$\map {q_3} 2 = \dfrac {2^{3 - 1} - 1} 3 = 1$
which is square.
When $p = 7$:
:$\map {q_7} 2 = \dfrac {2^{7 - 1} - 1} 7 = \dfrac {63} 7 = 9$
which is square.
To show that these are the only ones, we observe that since $p$ is an odd prime, write:
:$p = 2 n + 1$ for $n \ge 1$.
Let $\map {q_p} 2$ be a square.
Then $2^{p - 1} - 1 = p x^2$ for some integer $x$.
Note that:
:$2^{p - 1} - 1 = 2^{2 n} - 1 = \paren {2^n - 1} \paren {2^n + 1}$
and we have:
:$\gcd \set {2^n - 1, 2^n + 1} = \gcd \set {2^n - 1, 2} = 1$
so $2^n - 1$ and $2^n + 1$ are coprime.
Hence there are $2$ cases:
Theorem: Smaller Elements of Pythagorean Triple not both Odd

Let $\left({x, y, z}\right)$ be a Pythagorean triple, i.e. integers such that $x^2 + y^2 = z^2$.
Then $x$ and $y$ cannot both be odd.

Proof:
{{AimForCont}} $x$ and $y$ are both odd such that:
:$\exists z \in \Z: x^2 + y^2 = z^2$
Then:
:$x^2 + y^2 \equiv 1 + 1 \equiv 2 \pmod 4$
But from Square Modulo 4:
:$z^2 \equiv 0 \pmod 4$ or $z^2 \equiv 1 \pmod 4$
Thus $x^2 + y^2$ can not be square.
It follows by Proof by Contradiction that  $x$ and $y$ cannot both be odd.
{{qed}}
Category:Pythagorean Triples
o1vtbu7f6w8n47oqvi0eo9kkmzt1yyy
Theorem: Every Element is Directed and Every Two Elements are Included in Third Element implies Union is Directed

Let $P = \struct {S, \preceq}$ be an ordered set.
Let $A$ be a set of subsets of $S$.
Let
:$\forall X \in A: X$ is directed.
Let
:$\forall X, Y \in A: \exists Z \in A: X \cup Y \subseteq Z$
Then $\bigcup A$ is directed.

Proof:
Let $x, y \in \bigcup A$.
By definition of union:
:$\exists X \in A: x \in X$
and
:$\exists Y \in A: y \in Y$
By assumption:
:$\exists Z \in A: X \cup Y \subseteq Z$
By definition of union:
:$x, y \in X \cup Y$
By definition of subset:
:$x, y \in Z$
By assumption:
:$Z$ is directed.
By definition of directed subset:
:$\exists z \in Z: x \preceq z \land y \preceq z$
Thus by definition of union:
:$z \in \bigcup A$
Thus
:$x \preceq z \land y \preceq z$
Hence $\bigcup A$ is directed.
{{qed}}
Theorem: Every Element is Lower implies Union is Lower

Let $\struct {S, \preceq}$ be an ordered set.
Let $A$ be a set of subsets of $S$.
Let
:$\forall X \in A: X$ is a lower section.
Then $\bigcup A$ is a lower section.

Proof:
Let $x \in \bigcup A, y \in S$ such that:
:$y \preceq x$
By definition of union:
:$\exists X \in A: x \in X$
By assumption:
:$X$ is a lower section.
By definition of lower section:
:$y \in X$
Thus by definition of union:
:$y \in \bigcup A$
{{qed}}
Theorem: If Element Does Not Belong to Ideal then There Exists Prime Ideal Including Ideal and Excluding Element

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a distributive lattice.
Let $I$ be an ideal in $L$.
Let $x$ be an element of $S$.
Suppose $x \notin I$
Then there exists a prime ideal $P$ in $L$: $I \subseteq P$ and $x \notin P$

Proof:
By Upper Closure of Element is Filter:
:$x^\succeq$ is a filter.
We will prove that
:$I \cap x^\succeq = \O$
{{AimForCont}}:
:$\exists y: y \in I \cap x^\succeq$
By definition of intersection:
:$y \in I$ and $y \in x^\succeq$
By definition of upper closure of element:
:$x \preceq y$
By definition of lower section:
:$x \in I$
This contradicts $x \notin I$
{{qed|lemma}}
Thus by If Ideal and Filter are Disjoint then There Exists Prime Ideal Including Ideal and Disjoint from Filter:
:there exists a prime ideal $P$ in $L$: $I \subseteq P$ and $P \cap x^\succeq = \O$
By definition of reflexivity:
:$x \preceq x$
By definition of upper closure of element:
:$x \in x^\succeq$
Thus by definitions of intersection and empty set:
:$x \notin P$
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -x by Logarithm of x

Let $\ln t$ denote the natural logarithm function for real $t > 0$.
Let $e^{-t}$ denote the real exponential.
Then:
:$\ds \int_{0^+}^{\mathop \to +\infty} \ln t \, e^{-t} \rd t = - \gamma$
where the {{LHS}} is an improper integral, and $\gamma$ is the Euler-Mascheroni Constant.

Proof:
{{begin-eqn}}
{{eqn | l = \int_{0^+}^{ \mathop \to +\infty} \ln t \, e^{-t} \rd t
      | r = \int_{0^+}^{ \mathop \to +\infty} t^{1 - 1} \ln t \, e^{-t} \rd t
}}
{{eqn | r = \map {\Gamma'} 1
      | c = Derivative of Gamma Function
}}
{{eqn | r = -\gamma
      | c = Derivative of Gamma Function at $1$
}}
{{end-eqn}}
{{qed}}
Theorem: Bottom not in Proper Filter

Let $L = \struct {S, \preceq}$ be a bounded below preordered set.
Let $F$ be a filter on $L$.
Then $F$ is proper filter {{iff}} $\bot \notin F$
where $\bot$ denotes the smallest element of $S$.

Proof:
=== Sufficient Condition ===
Suppose:
:$F$ is proper.
By definition of proper subset:
:$F \subseteq S$ and $F \ne S$
By definitions of set equality and subset:
:$\exists x: x \in S \land x \notin F$
By definition of smallest element:
:$\bot \preceq x$
Thus by definition of upper section:
:$\bot \notin F$
{{qed|lemma}}
Theorem: If Ideal and Filter are Disjoint then There Exists Prime Filter Including Filter and Disjoint from Ideal

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a distributive lattice.
Let $I$ be an ideal in $L$.
Let $F$ be a filter on $L$ such that
:$F \cap I = \O$
Then there exists a prime filter $P$ in $L$:
$F \subseteq P$ and $P \cap I = \O$

Proof:
By Dual Distributive Lattice is Distributive:
:$L^{-1}$ is a distributive lattice
where $L^{-1} = \struct {S, \succeq}$ denotes the dual of $L$.
By Filter is Ideal in Dual Ordered Set:
:$I' := F$ as an ideal in $L^{-1}$.
By Ideal is Filter in Dual Ordered Set:
:$F' := I$ as a filter on $L^{-1}$.
By assumption:
:$I' \cap F' = \O$
By If Ideal and Filter are Disjoint then There Exists Prime Ideal Including Ideal and Disjoint from Filter:
:there exists prime ideal $P'$ in $L^{-1}$: $I' \subseteq P'$ and $P' \cap F' = \O$
By Prime Filter is Prime Ideal in Dual Lattice:
:$P := P'$ as a prime filter on $L$.
Thus there exists prime filter $P$ on $L$: $F \subseteq P$ and $P \cap I = \O$
{{qed}}
Theorem: Dual Distributive Lattice is Distributive

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a lattice.
Then
:$L$ is a distributive lattice
{{iff}}
:$L^{-1}$ is a distributive lattice
where $L^{-1} = \struct {S, \succeq}$ denotes the dual of $L$.

Proof:
=== Sufficient Condition ===
Let $L$ be a distributive lattice.
By Dual of Lattice Ordering is Lattice Ordering:
:$L^{-1}$ is lattice.
Let $x, y, z \in S$.
$\vee'$ and $\wedge'$ denotes join and meet in $L^{-1}$.
Thus
{{begin-eqn}}
{{eqn | l = x \wedge' \paren {y \vee' z}
      | r = x \wedge' \paren {y \wedge z}
      | c = Join is Dual to Meet
}}
{{eqn | r = x \vee \paren {y \wedge z}
      | c = Join is Dual to Meet
}}
{{eqn | r = \paren {x \vee y} \wedge \paren {x \vee z}
      | c = {{Defof|Distributive Lattice}}
}}
{{eqn | r = \paren {x \wedge' y} \wedge \paren {x \wedge' z}
      | c = Join is Dual to Meet
}}
{{eqn | r = \paren {x \wedge' y} \vee' \paren {x \wedge' z}
      | c = Join is Dual to Meet
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Exchange of Rows as Sequence of Other Elementary Row Operations

Let $\mathbf A$ be an $m \times n$ matrix.
Let $i, j \in \closedint 1 m: i \ne j$
Let $r_k$ denote the $k$th row of $\mathbf A$ for $1 \le k \le m$:
:$r_k = \begin {pmatrix} a_{k 1} & a_{k 2} & \cdots & a_{k n} \end {pmatrix}$
Let $e$ be the elementary row operation acting on $\mathbf A$ as:
{{begin-axiom}}
{{axiom | n = \text {ERO} 3
        | t = Interchange rows $i$ and $j$
        | m = r_i \leftrightarrow r_j
}}
{{end-axiom}}
Then $e$ can be expressed as a finite sequence of exactly $4$ instances of the other two elementary row operations.
{{begin-axiom}}
{{axiom | n = \text {ERO} 1
        | t = For some $\lambda \in K_{\ne 0}$, multiply row $i$ by $\lambda$
        | m = r_i \to \lambda r_i
}}
{{axiom | n = \text {ERO} 2
        | t = For some $\lambda \in K$, add $\lambda$ times row $j$ to row $i$
        | m = r_i \to r_i + \lambda r_j
}}
{{end-axiom}}

Proof:
In the below:
:$r_i$ denotes the initial state of row $i$
:$r_j$ denotes the initial state of row $j$
:$r_i'$ denotes the state of row $i$ after having had the latest elementary row operation applied
:$r_j'$ denotes the state of row $j$ after having had the latest elementary row operation applied.
$(1)$: Apply $\text {ERO} 2$ to row $j$ for $\lambda = 1$:
:$r_j \to r_j + r_i$
After this operation:
{{begin-eqn}}
{{eqn | l = r_i'
      | r = r_i
}}
{{eqn | l = r_j'
      | r = r_i + r_j
}}
{{end-eqn}}
{{qed|lemma}}
$(2)$: Apply $\text {ERO} 2$ to row $i$ for $\lambda = -1$:
:$r_i \to r_i + \paren {-r_j}$
After this operation:
{{begin-eqn}}
{{eqn | l = r_i'
      | r = r_i - \paren {r_i + r_j}
}}
{{eqn | r = -r_j
}}
{{eqn | l = r_j'
      | r = r_i + r_j
}}
{{end-eqn}}
{{qed|lemma}}
$(3)$: Apply $\text {ERO} 2$ to row $j$ for $\lambda = 1$:
:$r_j \to r_j + r_i$
After this operation:
{{begin-eqn}}
{{eqn | l = r_i'
      | r = -r_j
}}
{{eqn | l = r_j'
      | r = r_i + r_j - r_j
}}
{{eqn | r = r_i
}}
{{end-eqn}}
{{qed|lemma}}
$(4)$: Apply $\text {ERO} 1$ to row $i$ for $\lambda = -1$:
:$r_i \to -r_i$
After this operation:
{{begin-eqn}}
{{eqn | l = r_i'
      | r = -\paren {-r_j}
}}
{{eqn | r = r_j
}}
{{eqn | l = r_j'
      | r = r_i
}}
{{end-eqn}}
{{qed|lemma}}
Thus, after all the $4$ elementary row operations have been applied, we have:
{{begin-eqn}}
{{eqn | l = r_i'
      | r = r_j
}}
{{eqn | l = r_j'
      | r = r_i
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Proper Filter is Included in Ultrafilter in Boolean Lattice

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a Boolean lattice.
Let $F$ be a proper filter on $L$.
Then there exists ultrafilter $G$ on $L$: $F \subseteq G$

Proof:
By Singleton of Bottom is Ideal:
:$I := \set \bot$ is an ideal in $L$.
where $\bot$ denotes the bottom of $L$.
We will prove that
:$F \cap I = \O$
Let $x \in I$.
By definition of singleton:
:$x = \bot$
Thus by Bottom not in Proper Filter:
:$x \notin F$
{{qed|lemma}}
By If Ideal and Filter are Disjoint then There Exists Prime Filter Including Filter and Disjoint from Ideal:
:there exists a prime filter $G$ on $L$: $F \subseteq G$ and $G \cap I = \O$
By definition of singleton:
:$\bot \in I$
By definitions of empty set and intersection:
:$\bot \notin G$
By Bottom not in Proper Filter:
:$G$ is proper.
Thus by Proper and Prime iff Ultrafilter in Boolean Lattice:
:$G$ is ultrafilter.
Thus $F \subseteq G$
{{qed}}
Theorem: Seven Different Frieze Groups

There are $7$ different frieze groups.

Proof:
{{ProofWanted|Lots of background work needed.}}
Theorem: Way Below iff Second Operand Preceding Supremum of Prime Ideal implies First Operand is Element of Ideal

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a distributive complete lattice.
Let $x, y \in S$.
Then $x \ll y$ {{iff}}:
:for every prime ideal $P$ in $L$: $y \preceq \sup P \implies x \in P$

Proof:
=== Sufficient Condition ===
The result follows by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal.
{{qed|lemma}}
Theorem: Lower Closure is Prime Ideal for Prime Element

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a lattice.
Let $p \in S$ be a prime element.
Then $p^\preceq$ is a prime ideal.

Proof:
Let $x, y \in S$ such that
:$x \wedge y \in p^\preceq$
By definition of lower closure of element:
:$x \wedge y \preceq p$
By Characterization of Prime Ideal:
:$x \preceq p$ or $y \preceq p$
Thus by definition of lower closure of element:
:$x \in p^\preceq$ or $y \in p^\preceq$
{{qed}}
Theorem: Prime is Pseudoprime (Order Theory)

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be an up-complete lattice.
Let $p \in S$ be a prime element.
Then $p$ is pseudoprime.

Proof:
By Lower Closure is Prime Ideal for Prime Element:
:$p^\preceq$ is prime ideal.
By Supremum of Lower Closure of Element:
:$ \sup \left({ p^\preceq }\right) = p$
Hence $p$ is pseudoprime.
{{qed}}
Theorem: Regular Heptagon is Smallest with no Compass and Straightedge Construction

The regular heptagon is the smallest regular polygon (smallest in the sense of having fewest sides) that cannot be constructed using a compass and straightedge construction.

Proof:
{{tidy}}
{{MissingLinks}}
A theorem states that:
"The n-gon is constructible by compass and straightedge construction if and only if $n = 2^kn_0$, with $k \in \mathbb{Z}_{\geq0}$ and $n_0$ the product of any number of distinct Fermat primes."
Note that 3 and 5 are both Fermat primes, so their respective n-gon are both constructible; and $4$ is just a power of $2$, so the 4-gon also constructible. 
Lastly, since 6 is the product of 2 and 3, the 6-gon is constructible as well. Hence, we remain with 7, which does not satisfy the theorem's criteria; and thus the 7-gon is the smallest regular polygon that cannot be constructed using a compass and straightedge construction.
{{qed}}
Theorem: Smallest Prime Number whose Period is of Maximum Length

$7$ is the smallest prime number the period of whose reciprocal, when expressed in decimal notation, is maximum:
:$\dfrac 1 7 = 0 \cdotp \dot 14285 \dot 7$

Proof:
From Maximum Period of Reciprocal of Prime, the maximum period of $\dfrac 1 p$ is $p - 1$.
:$\dfrac 1 2 = 0 \cdotp 5$: not recurring.
:$\dfrac 1 3 = 0 \cdotp \dot 3$: recurring with period $1$.
:$\dfrac 1 5 = 0 \cdotp 2$: not recurring.
:$\dfrac 1 7 = 0 \cdotp \dot 14285 \dot 7$: recurring with period $6$.
{{qed}}
Theorem: Characterization of Pseudoprime Element by Finite Infima

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a continuous lattice.
Let $p \in S$ be a pseudoprime element.
Let $A$ be a non-empty finite subset of $S$ such that
:$\inf A \ll p$
where $\ll$ denotes the way below relation.
Then $\exists a \in A: a \preceq p$

Proof:
By definition of pseudoprime element:
:there exists a prime ideal $P$ in $L$: $p = \sup P$
By definition of way below closure:
:$\inf A \in p^\ll$
By definition of reflexivity:
:$p \preceq \sup P$
By Continuous iff Way Below Closure is Ideal and Element Precedes Supremum:
:$p^\ll \subseteq P$
By definition of subset:
:$\inf A \in P$
Thus by Characterization of Prime Ideal by Finite Infima
:$\exists a \in A: a \in P$
By definition of up-complete:
:$P$ admits a supremum.
By definition of supremum:
:$p$ is upper bound for $P$.
Thus by definition of upper bound:
:$a \preceq p$
{{qed}}
Theorem: Elementary Row Operations as Matrix Multiplications/Corollary

Let $\mathbf X$ and $\mathbf Y$ be two $m \times n$ matrices that differ by exactly one elementary row operation.
Then there exists an elementary row matrix of order $m$ such that:
:$\mathbf {E X} = \mathbf Y$

Proof:
Let $e$ be the elementary row operation such that $e \paren {\mathbf X} = \mathbf Y$.
Then this result follows immediately from Elementary Row Operations as Matrix Multiplications:
:$e \paren {\mathbf X} = \mathbf {E X} = \mathbf Y$
where $\mathbf E = e \paren {\mathbf I}$.
{{qed}}
Theorem: Cyclotomic Polynomial of Prime Index

Let $p$ be a prime number.
The '''$p$th cyclotomic polynomial''' is:
:$\map {\Phi_p} x = x^{p - 1} + x^{p - 2} + \cdots + x + 1$

Proof:
From Product of Cyclotomic Polynomials:
:$\map {\Phi_p} x \map {\Phi_1} x = x^p - 1$
Thus from Sum of Geometric Sequence:
:$\map {\Phi_p} x = \dfrac {x^p - 1} {x - 1} = x^{p - 1} + x^{p - 2} + \cdots + x + 1$
{{qed}}
Theorem: Product of Cyclotomic Polynomials

Let $n > 0$ be a (strictly) positive integer.
Then:
:$\ds \prod_{d \mathop \divides n} \map {\Phi_d} x = x^n - 1$
where:
:$\map {\Phi_d} x$ denotes the $d$th cyclotomic polynomial
:the product runs over all divisors of $n$.

Proof:
From the Polynomial Factor Theorem and Complex Roots of Unity in Exponential Form:
:$\ds x^n - 1 = \prod_\zeta \paren {x - \zeta}$
where the product runs over all complex $n$th roots of unity.
In the {{LHS}}, each factor $x - \zeta$ appears exactly once, in the factorization of $\map {\Phi_d} x$ where $d$ is the order of $\zeta$.
{{explain|The above statement needs justification.}}
Thus the polynomials are equal.
{{qed}}
Theorem: First Cyclotomic Polynomial

The '''first cyclotomic polynomial''' is:
:$\map {\Phi_1} x = x - 1$

Proof:
By definition:
:$\ds \map {\Phi_1} x = \prod_\zeta \paren {x - \zeta}$
where the product runs over all primitive complex first roots of unity.
A root of unity has order $1$ {{iff}} it equals $1$.
{{explain|The above statement needs justification, with reference to the definition of the order of a root of unity.}}
Hence the only factor is $x - 1$.
{{MissingLinks|Factor of Polynomial -- for which we appear not to have a page.}}
Category:Examples of Cyclotomic Polynomials
6k5ft4dqn0f1f1394hv2m9aogku3479
Theorem: Cyclotomic Polynomial has Integer Coefficients

Let $n \in \Z_{>0}$ be a positive integer.
Then the $n$th cyclotomic polynomial $\map {\Phi_n} x$ has integer coefficients.

Proof:
The proof proceeds by strong induction on $n$.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$\map {\Phi_n} x$ has integer coefficients
Theorem: Formal Derivative of Polynomials Satisfies Leibniz's Rule

Let $R$ be a commutative ring with unity.
Let $R \sqbrk X$ be the polynomial ring over $R$.
Let $f, g \in R \sqbrk X$ be polynomials.
Let $f'$ and $g'$ denote their formal derivatives.
Then:
:$\paren {f g}' = f g' + f' g$

Proof:
Both sides are bilinear functions of $f$ and $g$, so it suffices to verify the equality in the case where $\map f X = X^n$ and $\map g x = X^m$.
Then:
:$\paren {X^n X^m}' = \paren {n + m} X^{n + m - 1}$
and:
:$\paren {X^n}' X^m + X^n \paren {X^m}' = n X^{n - 1} X^m + m X^n X^{m - 1}$
{{qed}}
Category:Leibniz's Rule
Category:Polynomial Theory
alww1dgljeteqm3cmeyfwq3oc07fyyc
Theorem: Double Root of Polynomial is Root of Derivative

Let $R$ be a commutative ring with unity.
Let $f \in R \sqbrk X$ be a polynomial.
Let $a \in R$ be a root of $f$ with multiplicity at least $2$.
Let $f'$ denote the formal derivative of $f$.
Then $a$ is a root of $f'$.

Proof:
Because $a$ has multiplicity at least $2$, we can write:
:$\map f X = \paren {X - a}^2 \map g X$
with $\map g X \in R \sqbrk X$.
From Formal Derivative of Polynomials Satisfies Leibniz's Rule:
:$\map {f'} X = 2 \paren {X - a} \map g X + \paren {X - a}^2 \map {g'} X$
and thus:
:$\map {f'} a = 0$
{{qed}}
Category:Polynomial Theory
qj9lyzunerexnalc2ef06fhtjeyla9i
Theorem: 7 Prime Knots with 7 Crossings

There exist exactly $7$ prime knots which have exactly $7$ crossings.

Proof:
{{ProofWanted|Much background work to be done.}}
Theorem: Prime Divisors of Cyclotomic Polynomials

Let $n \ge 1$ be a positive integer.
Let $\map {\Phi_n} x$ denote the $n$th cyclotomic polynomial.
Let $a \in \Z$ be an integer such that $\map {\Phi_n} a \ne 0$.
Let $p$ be a prime divisor of $\map {\Phi_n} a$.
Then $p \equiv 1 \pmod n$ or $p \divides n$.

Proof:
Let $k$ be the order of $a$ modulo $p$.
By Element to Power of Multiple of Order is Identity, $k \divides p - 1$.
If $k = n$, the result follows.
Let $k < n$.
Then by Product of Cyclotomic Polynomials, there exists $d \divides k$ such that $p \divides \map {\Phi_d} a$.
Consequently, $a$ is a double root of $\Phi_d \Phi_n$ modulo $p$.
Again by Product of Cyclotomic Polynomials, $a$ is a double root of $x^n - 1$ modulo $p$.
Thus, by Double Root of Polynomial is Root of Derivative, $a$ is a root of the derivative of $x^n - 1$ modulo $p$, which is the constant polynomial $n$.
Thus $n \equiv 0 \pmod p$, for a nonzero constant polynomial has no roots.
{{qed}}
Theorem: Pack of Cards is Randomized by 7 Riffle Shuffles

A pack of cards is randomized by $7$ riffle shuffles.

Proof:
{{ProofWanted|Background work needed.}}
Theorem: Sum of Complex Indices of Real Number

Let $r \in \R_{> 0}$ be a (strictly) positive real number.
Let $\psi, \tau \in \C$ be complex numbers.
Let $r^\lambda$ be defined as the the principal branch of a positive real number raised to a complex number.
Then:
:$r^{\psi \mathop + \tau} = r^\psi \times r^\tau$

Proof:
Then:
{{begin-eqn}}
{{eqn | l = r^{\psi \mathop + \tau}
      | r = \map \exp {\paren {\psi + \tau} \ln r}
      | c = {{Defof|Power (Algebra)/Complex Number/Principal Branch/Positive Real Base|Principal Branch of Positive Real Number raised to Complex Number}}
}}
{{eqn | r = \map \exp {\psi \ln r + \tau \ln r}
}}
{{eqn | r = \map \exp {\psi \ln r} \, \map \exp {\tau \ln r}
      | c = Exponential of Sum
}}
{{eqn | r = r^\psi \times r^\tau
      | c = {{Defof|Power (Algebra)/Complex Number/Principal Branch/Positive Real Base|Principal Branch of Positive Real Number raised to Complex Number}}
}}
{{end-eqn}}
{{qed}}
Category:Powers
k3hqknj348ae2u78j6idayayc85fnij
Theorem: Universal Property of Free Modules

Let $R$ be a ring.
Let $M$ be a free $R$-module with basis $\set {e_i: i\in I}$.
Let $N$ be an $R$-module.
Let $\set {n_i:  i \in I}$ be a family of elements of $N$.
Then there exists a unique $R$-module homomorphism that maps $e_i$ to $n_i$ for all $i\in I$.

Proof:
Combine Free Module is Isomorphic to Free Module Indexed by Set and Universal Property of Free Module on Set.
{{handwaving}}
Category:Free Modules
Category:Module Theory
Category:Universal Properties
5dah6s5fykqiqimrzkusypeeibpbmzw