avewright/proofwiki-math huggingface dataset:
Theorem: Composite of Injection on Surjection is not necessarily Either

Let $f$ be an injection.
Let $g$ be a surjection.
Let $f \circ g$ denote the composition of $f$ with $g$.
Then it is not necessarily the case that $f \circ g$ is either a surjection or an injection.

Proof:
Let $X, Y, Z$ be sets defined as:
{{begin-eqn}}
{{eqn | l = X
      | r = \set {a, b, c}
      | c = 
}}
{{eqn | l = Y
      | r = \set {1, 2}
      | c = 
}}
{{eqn | l = Z
      | r = \set {z, y, z}
      | c = 
}}
{{end-eqn}}
Let $g: X \to Y$ be defined in two-row notation as:
:$\dbinom {a \ b \ c } {1 \ 2 \ 2}$
which is seen by inspection to be a surjection.
Let $f: Y \to Z$ be defined in two-row notation as:
:$\dbinom {1 \ 2} {x \ y}$
which is seen by inspection to be an injection.
The composition $f \circ g$ is seen to be:
:$\dbinom {a \ b \ c} {x \ y \ y}$
which is:
:not an injection (both $b$ and $c$ map to $y$)
:not a surjection (nothing maps to $z$).
Hence the result.
{{qed}}
Theorem: Group of Order 3 is Unique

There exists exactly $1$ group of order $3$, up to isomorphism:
:$C_3$, the cyclic group of order $3$.

Proof:
From Existence of Cyclic Group of Order n we have that one such group of order $3$ is the cyclic group of order $3$.
This is exemplified by the additive group of integers modulo $3$, whose Cayley table can be presented as:
{{:Modulo Addition/Cayley Table/Modulo 3}}{{qed|lemma}}
Consider an arbitrary group $\struct {G, \circ}$ whose identity element is $e$.
Let the underlying set of $G$ be:
:$G = \set {e, a, b}$
where $a, b \in G$ are arbitrary.
Since $e$ is the identity, we can start off the Cayley table for $G$ as:
:$\begin{array}{c|ccc}
\circ & e & a & b \\
\hline
e & e & a & b \\
a & a &   &   \\
b & b &   &   \\
\end{array}$
Consider the element at $a \circ a$.
We have that $a \circ a$ must be either $e$ or $b$, as from Group has Latin Square Property it cannot be $a$.
If $a \circ a = e$, then that leaves only $b$ to complete the middle row.
But $b$ already exists in the final column.
So $a \circ a$ cannot be $e$, so must be $b$.
Hence the Cayley table for $G$ so far is:
:$\begin{array}{c|ccc}
\circ  & e & a & b \\
\hline
e & e & a & b \\
a & a & b &   \\
b & b &   &   \\
\end{array}$
The rest of the table is completed by following the result that Group has Latin Square Property:
:$\begin{array}{c|ccc}
\circ  & e & a & b \\
\hline
e & e & a & b \\
a & a & b & e \\
b & b & e & a \\
\end{array}$
and it is seen by inspection that $G$ is indeed the cyclic group of order $3$.
{{qed}}
Theorem: Sequence of Powers of Number less than One

Let $x \in \R$.
Let $\sequence {x_n}$ be the sequence in $\R$ defined as $x_n = x^n$.
Then:
:$\size x < 1$ {{iff}} $\sequence {x_n}$ is a null sequence.

Proof:
=== Necessary Condition ===
{{refactor|level = basic}}
[For other proofs of the Necessary Condition visit here.]
{{:Sequence of Powers of Number less than One/Necessary Condition/Proof 1}}{{qed|lemma}}
Theorem: Sequence of Powers of Number less than One

Let $x \in \R$.
Let $\sequence {x_n}$ be the sequence in $\R$ defined as $x_n = x^n$.
Then:
:$\size x < 1$ {{iff}} $\sequence {x_n}$ is a null sequence.

Proof:
{{WLOG}}, assume that $x \ne 0$.
Observe that {{hypothesis}}:
:$0 < \size x < 1$
Thus by Ordering of Reciprocals:
:$\size x^{-1} > 1$
Define:
:$h = \size x^{-1} - 1 > 0$
Then:
:$x = \dfrac 1 {1 + h}$
By the binomial theorem, we have that:
:$\paren {1 + h}^n = 1 + n h + \cdots + h^n > n h$
because $h > 0$.
By Absolute Value Function is Completely Multiplicative, it follows that:
:$0 \le \size {x^n} = \size x^n = \dfrac 1 {\paren {1 + h}^n} < \dfrac 1 {n h}$
From Sequence of Reciprocals is Null Sequence:
:$\dfrac 1 n \to 0$ as $n \to \infty$
By the Multiple Rule for Real Sequences:
:$\dfrac 1 {n h} \to 0$ as $n \to \infty$
By the {{Corollary|Squeeze Theorem for Real Sequences}}:
:$\size {x^n} \to 0$
as $n \to \infty$.
Hence the result, by the definition of a limit.
Theorem: Sequence of Powers of Number less than One

Let $x \in \R$.
Let $\sequence {x_n}$ be the sequence in $\R$ defined as $x_n = x^n$.
Then:
:$\size x < 1$ {{iff}} $\sequence {x_n}$ is a null sequence.

Proof:
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
Suppose that:
:$\exists N \in \N: \size x^N < \epsilon$
Then the result follows by the definition of a limit, because:
:$\forall n \in \N: n \ge N \implies \size {x^n} = \size x^n \le \size x^N < \epsilon$
where Absolute Value Function is Completely Multiplicative is applied.
It remains to consider the case that:
:$\forall n \in \N: \size x^n \ge \epsilon$
By the Axiom of Archimedes, we can choose a natural number $M$ such that:
:$M > \dfrac 1 {\paren {1 - \size x} \epsilon}$
Then, by Sum of Geometric Sequence:
:$\ds M \epsilon \le \sum_{k \mathop = 0}^{M - 1} \size x^k = \frac {1 - \size x^M} {1 - \size x} < M \epsilon$ 
a contradiction.
Hence the result.
{{qed}}
Theorem: Sequence of Powers of Number less than One

Let $x \in \R$.
Let $\sequence {x_n}$ be the sequence in $\R$ defined as $x_n = x^n$.
Then:
:$\size x < 1$ {{iff}} $\sequence {x_n}$ is a null sequence.

Proof:
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
By the Axiom of Archimedes, there exists a natural number $M$ such that:
:$M > \dfrac 1 {\paren {1 - \size x} \epsilon}$
By the Well-Ordering Principle, there exists a smallest natural number $m$ such that:
:$\exists N \in \N: m > M \size x^N$
Note that:
:$m - 1 \le M \size x^{N + 1}$
By elementary algebra, it follows that:
:$1 - \dfrac 1 m = \dfrac {m - 1} m \le \size x < 1 - \dfrac 1 {M \epsilon}$
Hence, $m < M \epsilon$.
Therefore:
:$\size x^N < \epsilon$
By Absolute Value Function is Completely Multiplicative:
:$\forall n \in \N: n \ge N \implies \size {x^n} = \size x^n \le \size x^N < \epsilon$
Hence the result, by the definition of a limit.
{{qed}}
Theorem: Sequence of Powers of Number less than One

Let $x \in \R$.
Let $\sequence {x_n}$ be the sequence in $\R$ defined as $x_n = x^n$.
Then:
:$\size x < 1$ {{iff}} $\sequence {x_n}$ is a null sequence.

Proof:
Define:
:$\ds L = \inf_{n \mathop \in \N} \size x^n$
By the Continuum Property, such an $L$ exists in $\R$.
Clearly, $L \ge 0$.
{{AimForCont}} $L > 0$.
Then, by the definition of the infimum, we can choose $n \in \N$ such that $\size x^n < L \size x^{-1}$.
But then $\size x^{n + 1} < L$, which contradicts the definition of $L$.
Therefore, $L = 0$.
Let $\epsilon \in \R_{>0}$ be a strictly positive real number.
By the definition of the infimum, there exists an $N \in \N$ such that $\size x^N < \epsilon$.
It follows that:
:$\forall n \in \N: n \ge N \implies \size {x^n} = \size x^n \le \size x^N < \epsilon$
where Absolute Value Function is Completely Multiplicative is applied.
Hence the result, by the definition of a limit.
{{qed}}
Theorem: Set of Rotations is Subgroup of Symmetry Group

Let $G$ be a symmetry group.
Let $H$ be the subset of $G$ consisting of the rotations in $G$ about a given axis.
Then $H$ is a subgroup of $G$.

Proof:
{{ProofWanted|Needs a more formal definition of rotation. Surprised this hasn't already been covered properly.}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms

Let $R$ be a division ring.
Let $\norm {\, \cdot \,}_1: R \to \R_{\ge 0}$ and $\norm {\, \cdot \,}_2: R \to \R_{\ge 0}$ be norms on $R$.
Let $d_1$ and $d_2$ be the metrics induced by the norms $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ respectively.
{{TFAE|def = Equivalent Division Ring Norms}}

Proof:
=== Topologically Equivalent implies Convergently Equivalent ===
{{:Equivalence of Definitions of Equivalent Division Ring Norms/Topologically Equivalent implies Convergently Equivalent}}{{qed|lemma}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Topologically Equivalent implies Convergently Equivalent

Let $d_1$ and $d_2$ be topologically equivalent metrics.
Then:
:$d_1$ and $d_2$ are convergently equivalent metrics.

Proof:
Let $\sequence {x_n}$ converge to $l$ in $\norm {\, \cdot \,}_1$.
Let $\epsilon \in \R_{> 0}$ be given.
Let $\map {B_\epsilon^2} i$ denote the open ball centered on $l$ of radius $\epsilon$ in $\struct {R, \norm {\, \cdot \,}_2}$.
By Open Ball of Metric Space is Open Set then $\map {B_\epsilon^2} l$ is open set in $\struct {R, d_2}$.
Since $d_1$ and $d_2$ are topologically equivalent metrics then $\map {B_\epsilon^2} l$ is open set in $\struct {R, d_1}$.
By the definition of an open set in a metric space then:
:$\exists \delta \in \R_{> 0}: \map {B_\delta^1} l \subseteq \map {B_\epsilon^2} l$
Hence:
:$\forall x \in R: \norm {x - l}_1 < \delta \implies \norm {x - l}_2 < \epsilon$
Since $\sequence {x_n}$ converges to $l$ in $\norm {\, \cdot \,}_1$ then:
:$\exists N \in \N: \forall n \ge N: \norm {x_n - l}_1 < \delta$
Hence:
:$\exists N \in \N: \forall n \ge N: \norm {x_n - l}_2 < \epsilon$
Since $\sequence {x_n}$ and $\epsilon > 0$ were arbitrary then it has been shown that for all sequences $\sequence {x_n}$ in $R$: 
:$\sequence {x_n}$ converges to $l$ in $\norm {\, \cdot \,}_1 \implies \sequence {x_n}$ converges to $l$ in $\norm {\, \cdot \,}_2$. 
By a similar argument it is shown that for all sequences $\sequence {x_n}$ in $R$:
:$\sequence {x_n}$ converges to $l$ in $\norm {\, \cdot \,}_2 \implies \sequence {x_n}$ converges to $l$ in $\norm {\, \cdot \,}_1$. 
The result follows. 
{{qed}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Convergently Equivalent implies Null Sequence Equivalent

Let $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ satisfy:
:for all sequences $\sequence {x_n}$ in $R:\sequence {x_n}$ converges to $l$ in $\norm{\, \cdot \,}_1 \iff \sequence {x_n}$ is a converges to $l$ in $\norm {\, \cdot \,}_2$
Then for all sequences $\sequence {x_n}$ in $R$:
:$\sequence {x_n}$ is a null sequence in $\norm {\, \cdot \,}_1 \iff \sequence {x_n}$ is a null sequence in $\norm {\, \cdot \,}_2$

Proof:
Let $0_R$ be the zero of $R$, then:
:$\sequence {x_n}$ converges to $0_R$ in $\norm {\, \cdot \,}_1 \iff \sequence {x_n}$ converges to $0_R$ in $\norm {\, \cdot \,}_2$
Hence:
:$\sequence {x_n}$ is a null sequence in $\norm{\,\cdot\,}_1  \iff \sequence {x_n}$ is a null sequence in $\norm{\,\cdot\,}_2$ 
{{qed}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Null Sequence Equivalent implies Open Unit Ball Equivalent

Let $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ satisfy:
:for all sequences $\sequence {x_n}$ in $R:\sequence {x_n}$ is a null sequence in $\norm {\, \cdot \,}_1  \iff \sequence {x_n}$ is a null sequence in $\norm {\, \cdot \,}_2$ 
Then $\forall x \in R$:
:$\norm x_1 < 1 \iff \norm x_2 < 1$

Proof:
Let $x \in R$.
Let $\sequence {x_n}$ be the sequence defined by: $\forall n: x_n = x^n$.
{{begin-eqn}}
{{eqn | l = \norm x_1 < 1 \quad
      | o = \leadstoandfrom
      | c = $\sequence {x_n}$ is a null sequence in $\norm {\, \cdot \,}_1$
      | cc= Sequence of Powers of Number less than One in Normed Division Ring
}}
{{eqn | o = \leadstoandfrom
      | c = $\sequence {x_n}$ is a null sequence in $\norm {\, \cdot \,}_2$
      | cc= Assumption
}}
{{eqn | o = \leadstoandfrom
      | c = $\norm x_2 < 1$
      | cc= Sequence of Powers of Number less than One in Normed Division Ring
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Open Unit Ball Equivalent implies Norm is Power of Other Norm

Let $\norm {\, \cdot \,}_1$ and $\norm {\, \cdot \,}_2$ satisfy:
:$\forall x \in R: \norm x_1 < 1 \iff \norm x_2 < 1$ 
Then:
:$\exists \alpha \in \R_{> 0}: \forall x \in R: \norm x_1 = \norm x_2^\alpha$

Proof:
==== Case 1 ====
For all $x \in R: x \ne 0_R$, let $x$ satisfy $\norm x_1 \ge 1$.
Theorem: Product of Subgroups of Prime Power Order

Let $p$ be a prime number.
Let $G$ be a group of order $p^a k$, where:
:$a \in \Z_{>0}$ is a (strictly) positive integer
:$p$ is not a divisor of $k$.
Let $P \le G$ be a subgroup of $G$ of order $p^a$.
Let $Q \le G$ be a subgroup of $G$ of order $p^b$, where $0 < b \le a$.
Let it be the case that $Q$ is not a subgroup of $P$.
Then $P Q$ is not a subgroup of $G$.

Proof:
From Intersection of Subgroups is Subgroup, $P \cap Q$ is a subgroup of $P$.
Thus:
:$\order {P \cap Q} = p^c$ for some $c \in \Z$ such that $0 \le c \le a$
where $\order {P \cap Q}$ denotes the order of $P \cap Q$.
We have:
{{begin-eqn}}
{{eqn | l = \order {P Q}
      | r = \frac {\order P \order Q} {\order {P \cap Q} }
      | c = Order of Subgroup Product
}}
{{eqn | r = \frac {p^a p^b} {p^c}
      | c = 
}}
{{eqn | r = p^{a + b - c}
      | c = 
}}
{{end-eqn}}
{{AimForCont}} $P Q$ is a subgroup of $G$.
By Lagrange's Theorem (Group Theory):
:$\order {P Q} \divides \order G$
where $\divides$ denotes divisibility.
We have that $\order {P Q}$ is a power of $p$.
The highest power of $p$ which divides $\order G$ is $p^a$.
Thus $P Q$ could have order $p^a$ at most.
Thus:
:$a + b - c \le a$
That is:
:$b \le c$
But $P \cap Q$ is a subgroup of $P$.
Hence it must be the case that $b = c$.
Thus:
:$P \cap Q = Q$
and so $Q$ is a subgroup of $P$.
This contradicts the fact that $Q$ is not a subgroup of $P$.
It must follow that $P Q$ is not a subgroup of $G$.
{{qed}}
Theorem: Basis Theorem

$H$ is a basis for $E$ {{iff}} it contains exactly $n$ elements.

Proof:
By hypothesis, let $H$ be a linearly independent subset of $E$
Theorem: Generator of Vector Space is Basis iff Cardinality equals Dimension

:$G$ is a basis for $E$ {{iff}} $\card G = n$.

Proof:
=== Necessary Condition ===
Let $G$ be a basis for $E$.
From Cardinality of Basis of Vector Space, $\card G = n$.
{{qed|lemma}}
Theorem: ISBN-10 is Error-Correcting Code/Transposition Error

If any two of the first $9$ digits are transposed, the check digit will be wrong.

Proof:
{{ProofWanted|Ongoing}}
Category:ISBN-10 is Error-Correcting Code
mwbruqai92ntf6l904fwb5runnoin1b
Theorem: ISBN-10 is Error-Correcting Code/Transmission Error

If an error has been made in any one of the first $9$ digits, the check digit will be wrong.

Proof:
Let $S$ denote an ISBN-$10$ whose $k$th digit is $d_k$.
Let $d_S$ denote the check digit of $S$.
Let $S'$ denote the ISBN-$10$ $S$ whose $n$th digit has been transmitted incorrectly, as $d'_n$.
Let $d'_S$ denote the check digit calculated on $S'$ according to the algorithm via which calculated $d_S$ on $S$.
It will be demonstrated that $d'_S \ne d_S$.
By definition of ISBN-$10$:
:$d_S = \ds \sum_{k \mathop = 1}^9 k d_k \pmod {11}$
where $d_k$ is assigned the symbol $X$ if it calculates to $10$.
Then:
:$d'_S = \ds \sum_{k \mathop = 1}^9 k d_k - n d_n + n d'_n \pmod {11}$
and so:
:$d'_S - d_S = n \paren {d'_n - d_n} \pmod {11}$
It follows that:
:$d'_S - d_S \ne 0$
and so the check digit on $d_S$ is the incorrect check digit for $S'$.
{{qed}}
Theorem: Cardinality of Master Code

Let $\map V {n, p}$ be a master code of length $n$ modulo $p$.
Then there are $p^n$ elements of $\map V {n, p}$.

Proof:
For each term of a sequence in $\map V {n, p}$ there are $p$ possible values.
There are $n$ such terms.
Hence there are $\underbrace {p \times p \times \cdots \times p}_{n \text { times} } = p^n$ different possible sequences in $\map V {n, p}$.
{{qed}}
Theorem: Master Code forms Vector Space

Let $\map V {n, p}$ be a master code of length $n$ modulo $p$.
Then $\map V {n, p}$ forms a vector space over $\Z_p$ of $n$ dimensions.

Proof:
Recall the vector space axioms:
{{:Axiom:Vector Space Axioms}}
First, the set of sequences $\tuple {x_1, x_2, \ldots, x_n}$, for $x_1, x_2, \ldots, x_n \in \Z_p$, has to be shown to fulfil the abelian group axioms.
This follows from:
:Integers Modulo m under Addition form Cyclic Group
and:
:Cyclic Group is Abelian.
{{ProofWanted|needs to be finished off, but it's tedious and I lack the patience tonight.}}
Theorem: Conditions Satisfied by Linear Code

Let $p$ be a prime number.
Let $\Z_p$ be the set of residue classes modulo $p$.
Let $C := \tuple {n, k}$ be a linear code of a master code $\map V {n, p}$.
Then $C$ satisfies the following conditions:
:$(C \, 1): \quad \forall \mathbf x, \mathbf y \in C: \mathbf x + \paren {-\mathbf y} \in C$
:$(C \, 2): \quad \forall \mathbf x \in C, m \in \Z_p: m \times \mathbf x \in C$
where $+$ and $\times$ are the operations of codeword addition and codeword multiplication respectively.
{{expand|Add a page defining the difference between codewords.}}

Proof:
From Master Code forms Vector Space, $\map V {n, p}$ is a vector space.
By definition, $\tuple {n, k}$ is a subspace of $\map V {n, p}$.
The result follows by the fact that a subspace is itself a vector space.
{{finish|I lose patience with the fine detail.}}
Theorem: Hamming Distance is Distance Function

Let $\map V {n, p}$ be a master code.
Let $d: V \times V \to \Z$ be the mapping defined as:
:$\forall u, v \in V: \map d {u, v} =$ the Hamming distance between $u$ and $v$
that is, the number of corresponding terms at which $u$ and $v$ are different.
Then $d$ defines a distance function in the sense of a metric space.

Proof:
It is to be demonstrated that $d$ satisfies all the metric space axioms.
Let $u, v, w \in \map V {n, p}$ be arbitrary.
Theorem: Minimum Distance of Linear Code is Smallest Weight of Non-Zero Codeword

Let $C$ be a linear $\tuple {n, k}$-code whose master code is $\map V {n, p}$.
Let $\map d C$ denote the minimum distance of $C$.
Then:
:$\map d C = \ds \min_{u \mathop \in C} \map w u$
where $\map w u$ denotes the weight of $u$.

Proof:
Let $f := \ds \min_{u \mathop \in C} \map w u$.
Let $\mathbf 0$ denote the codeword in $\map V {n, p}$ consisting of all zeroes.
As $C$ is a subspace of $\map V {n, p}$, we have that $\mathbf 0 \in C$.
Let $w$ be a codeword with weight $f$.
Then:
:$\map d {w, \mathbf 0} = f$
so $f \ge \map d C$.
Let $u, v \in C$ such that $\map d {u, v} = \map d C$.
We have that $C$ is a linear code.
Therefore:
:$u - v \in C$
where $u - v$ denotes the difference between $u$ and $v$.
But $u - v$ has weight $\map d C$.
Thus:
:$\map d C \ge f$
and it follows that $\map d C = f$.
{{qed}}
Theorem: Error Detection Capability of Linear Code

Let $C$ be a linear code.
Let $C$ have a minimum distance $d$.
Then $C$ detects $d - 1$ or fewer transmission errors.

Proof:
Let $C$ be a linear code whose master code is $V$.
Let $c \in C$ be a transmitted codeword.
Let $v$ be the received word from $c$.
By definition, $v$ is an element of $V$.
Let $v$ have a Hamming distance $f$ from $c$, where $f \le d - 1$.
Thus there have been $f$ transmission errors.
As $d$ is the minimum distance it is clear that $v$ cannot be a codeword of $C$.
Hence it can be understood that $C$ has detected that $v$ has as many as $d - 1$ transmission errors.
{{Qed}}
Theorem: Error Correction Capability of Linear Code

Let $C$ be a linear code.
Let $C$ have a minimum distance $d$.
Then $C$ corrects $e$ transmission errors for all $e$ such that $2 e + 1 \le d$.

Proof:
Let $C$ be a linear code whose master code is $V$.
Let $c \in C$ be a transmitted codeword.
Let $v$ be the received word from $c$.
By definition, $v$ is an element of $V$.
Let $v$ have a Hamming distance $e$ from $c$, where $2 e + 1 \le d$.
Thus there have been $e$ transmission errors.
{{AimForCont}} $c_1$ is a codeword of $C$, distinct from $c$, such that $\map d {v, c_1} \le e$.
Then:
{{begin-eqn}}
{{eqn | l = \map d {c, c_1}
      | o = \le
      | r = \map d {c, v} + \map d {v, c_1}
      | c = 
}}
{{eqn | o = \le
      | r = e + e
      | c = 
}}
{{eqn | o = <
      | r = d
      | c = 
}}
{{end-eqn}}
So $c_1$ has a Hamming distance from $c$ less than $d$.
But $C$ has a minimum distance $d$.
Thus $c_1$ cannot be a codeword of $C$.
From this contradiction it follows that there is no codeword of $C$ closer to $v$ than $c$.
Hence there is a unique codeword of $C$ which has the smallest Hamming distance from $v$.
Hence it can be understood that $C$ has corrected the transmission errors of $v$.
{{Qed}}
Theorem: Golay Ternary Code has Minimum Distance 5

The Golay ternary code has a minimum distance of $5$.

Proof:
Let $C$ denote the Golay ternary code.
By inspection of the standard generator matrix $G$ of $C$:
:$G := \begin{pmatrix}
1 & 0 & 0 & 0 & 0 & 0 & 0 & 1 & 2 & 2 & 1 \\
0 & 1 & 0 & 0 & 0 & 0 & 1 & 0 & 1 & 2 & 2 \\
0 & 0 & 1 & 0 & 0 & 0 & 2 & 1 & 0 & 1 & 2 \\
0 & 0 & 0 & 1 & 0 & 0 & 2 & 2 & 1 & 0 & 1 \\
0 & 0 & 0 & 0 & 1 & 0 & 1 & 2 & 2 & 1 & 0 \\
0 & 0 & 0 & 0 & 0 & 1 & 1 & 1 & 1 & 1 & 1 
\end{pmatrix}$
it is seen that the smallest weight of all the codewords of $C$ that can be found in $G$ is $5$.
So it is immediately seen that the minimum distance of $C$ is at least $5$.
It remains to be shown that the minimum distance of $C$ is no more than $5$.
{{ProofWanted}}
Theorem: Golay Ternary Code Corrects 2 Errors

The Golay ternary code corrects $2$ transmission errors.

Proof:
We have that Golay Ternary Code has Minimum Distance 5.
The result follows from Error Correction Capability of Linear Code.
{{qed}}
Theorem: Equivalence of Definitions of Equivalent Division Ring Norms/Open Unit Ball Equivalent implies Norm is Power of Other Norm/Lemma 1

:$\norm {\, \cdot \,}_1$ is the trivial norm.

Proof:
We prove the contrapositive.
Let $\norm {\, \cdot \,}_1$ be a nontrivial norm.
Then:
:$\exists y \in R: \norm y_1 \ne 0, \norm y_1 \ne 1$.
By Real Numbers form Totally Ordered Field either $\norm y_1 < 1$ or $\norm y_1 > 1$.
Suppose $\norm y_1 > 1$.
By Norm axiom $(\text N 1)$: Positive Definiteness:
:$y \ne 0_R$
By Norm of Inverse in Division Ring:
:$\norm {y^{-1} }_1 = \dfrac 1 {\norm y_1} < 1$
So either $\norm y_1 < 1$ or $\norm {y^{-1} }_1 < 1$
So:
:$\exists x \in R, x \ne 0_R:\norm x_1 < 1$
The theorem now follows by the Rule of Transposition. 
{{qed}}
Category:Equivalence of Definitions of Equivalent Division Ring Norms
9a4r3wlx5t5swutsh3fxwjvzvq6nrr6
Theorem: Syndrome is Zero iff Vector is Codeword

Let $C$ be a linear $\tuple {n, k}$-code whose master code is $\map V {n, p}$
Let $G$ be a (standard) generator matrix for $C$.
Let $P$ be a standard parity check matrix for $C$.
Let $w \in \map V {n, p}$.
Then the syndrome of $w$ is zero {{iff}} $w$ is a codeword of $C$.

Proof:
Let $G = \paren {\begin{array} {c|c} \mathbf I & \mathbf A \end{array} }$.
Let $c \in \map V {n, p}$.
Then, by definition of $G$, $c$ is a codeword of $C$ {{iff}} $c$ is of the form $u G$, where $u \in \map V {k, p}$.
Thus $c \in C$ {{iff}}:
{{begin-eqn}}
{{eqn | l = c
      | r = u G
      | c = 
}}
{{eqn | r = u \paren {\begin{array} {c {{!}} c} \mathbf I & \mathbf A \end{array} }
      | c = 
}}
{{eqn | r = \paren {\begin{array} {c {{!}} c} u & v \end{array} }
      | c = 
}}
{{end-eqn}}
where:
:$v = u \mathbf A$
:$\paren {\begin{array} {c|c} u & v \end{array} }$ denotes the $1 \times n$ matrix formed from the $k$ elements of $u$ and the $n - k$ elements of $v$.
Let $w \in \map V {n, p}$.
$w$ can be expressed in the form:
:$w = \paren {\begin{array} {c|c} u_1 & v_1 \end{array} }$
where $u_1 \in \map V {k, p}$.
The syndrome of $v$ is then calculated as:
{{begin-eqn}}
{{eqn | l = \map S v
      | r = \paren {\begin{array} {c {{!}} c} -\mathbf A^\intercal & \mathbf I \end{array} } w^\intercal
      | c = 
}}
{{eqn | r = \paren {\begin{array} {c {{!}} c} -\mathbf A^\intercal & \mathbf I \end{array} } \paren {\begin{array} {c {{!}} c} u_1^\intercal & v_1^\intercal \end{array} }
      | c = 
}}
{{eqn | r = -\mathbf A^\intercal u_1^\intercal + v_1^\intercal
      | c = 
}}
{{end-eqn}}
It follows that the syndrome of $w$ is zero {{iff}} $w$ is the concatenation of $u_1$ and $v_1$, where:
:$v_1^\intercal = \mathbf A^\intercal u_1^\intercal = \paren {u_1 \mathbf A}^\intercal$
Thus the syndrome of $w$ is zero {{iff}} $w$ is a codeword of $C$.
{{qed}}