avewright/proofwiki-math huggingface dataset:
Theorem: Functionally Complete Logical Connectives/Negation, Conjunction, Disjunction and Conditional

: $\set {\neg, \land, \lor, \implies}$: Not, And, Or and Implies

Proof:
From Functional Completeness over Finite Number of Arguments, it suffices to consider binary truth functions.
From Count of Truth Functions, there are $16$ of these.
These are enumerated in Binary Truth Functions, and are analysed in turn as follows.
Theorem: Functionally Complete Logical Connectives/Negation and Disjunction

:$\set {\neg, \lor}$: Not and Or

Proof:
From Functionally Complete Logical Connectives: Negation and Conjunction, $\set {\neg, \land}$ is functionally complete.
That is: any expression can be expressed in terms of $\neg$ and $\land$.
From De Morgan's laws: Conjunction, we have that:
:$p \land q \dashv \vdash \neg \paren {\neg p \lor \neg q}$
Thus all occurrences of $\land$ can be replaced by $\lor$ and $\neg$.
Thus any expression can be expressed in terms of $\neg$ and $\lor$.
That is: $\set {\neg, \lor}$ is functionally complete.
{{qed}}
Theorem: Functionally Complete Logical Connectives/Negation and Conjunction

:$\set {\neg, \land}$: Not and And

Proof:
From Functionally Complete Logical Connectives: Negation, Conjunction, Disjunction and Conditional, all sixteen of the binary truth functions can be expressed in terms of $\neg, \land, \lor, \implies$.
From Conjunction and Conditional, we have that:
:$p \implies q \dashv \vdash \neg \paren {p \land \neg q}$
From De Morgan's laws: Disjunction, we have that:
:$p \lor q \dashv \vdash \neg \paren {\neg p \land \neg q}$
So any instance of either $\implies$ or $\lor$ can be replaced identically with one using just $\neg$ and $\land$.
It follows that $\set {\neg, \land}$ is functionally complete.
{{qed}}
Theorem: Functionally Complete Logical Connectives/Negation and Conditional

:$\set {\neg, \implies}$: Not and Implies

Proof:
From Functionally Complete Logical Connectives: Negation and Conjunction, we can represent any boolean expression in terms of $\land$ and $\neg$.
From Conjunction and Conditional, we have that:
:$p \land q \dashv \vdash \neg \paren {p \implies \neg q}$
So it follows that we can replace all occurrences of $\land$ by $\implies$ and $\neg$.
Thus $\set {\neg, \implies}$ is functionally complete.
{{qed}}
Theorem: Functionally Complete Logical Connectives/Conjunction, Negation and Disjunction

:$\set {\neg, \land, \lor}$: Not, And and Or

Proof:
From the stronger results:
:Functionally Complete Logical Connectives: Negation and Disjunction:
::the set of logical connectives: $\set {\neg, \lor}$ is functionally complete
:Functionally Complete Logical Connectives: Negation and Conjunction:
::the set of logical connectives: $\set {\neg, \land}$ is functionally complete
it follows directly that $\set {\neg, \land, \lor}$ is likewise functionally complete.
{{qed}}
Category:Functional Completeness
eh8et9jrx7lv8b1gvg1ipjzycdrvr03
Theorem: Functionally Complete Logical Connectives/NAND

:$\set \uparrow$: NAND

Proof:
From Functionally Complete Logical Connectives: Negation and Conjunction, any boolean expression can be expressed in terms of $\land$ and $\neg$.
From NAND with Equal Arguments:
:$\neg p \dashv \vdash p \uparrow p$
From Conjunction in terms of NAND:
:$p \land q \dashv \vdash \paren {p \uparrow q} \uparrow \paren {p \uparrow q}$
demonstrating that $p \land q$ is expressed solely in terms of $\uparrow$.
Thus any boolean expression can be represented solely in terms of $\uparrow$.
That is, $\set \uparrow$ is functionally complete.
{{qed}}
Theorem: Functionally Complete Logical Connectives/NOR

:$\set \downarrow$: NOR

Proof:
From Functionally Complete Logical Connectives: Negation and Disjunction, any boolean expression can be expressed in terms of $\lor$ and $\neg$.
From NOR with Equal Arguments:
:$\neg p \dashv \vdash p \downarrow p$
From Disjunction in terms of NOR:
:$p \lor q \dashv \vdash \paren {p \downarrow q} \downarrow \paren {p \downarrow q}$
demonstrating that $p \lor q$ can be represented solely in terms of $\downarrow$.
That is, $\set \downarrow$ is functionally complete.
{{qed}}
Theorem: Functionally Complete Singleton Sets

The only binary logical connectives that form singleton sets which are functionally complete are NAND and NOR.

Proof:
Let $\uparrow$ and $\downarrow$ denote NAND and NOR respectively.
From:
: NAND is Functionally Complete
and
: NOR is Functionally Complete
the singleton sets $\left\{{\uparrow}\right\}$ and $\left\{{\downarrow}\right\}$ are functionally complete.
Suppose $\circ$ is a binary logical connective such that $\left\{{\circ}\right\}$ is a functionally complete set.
The unary logical connective $\neg$ has to be equivalent to some formula:
: $\cdots \circ \left({p \circ p}\right) \circ \cdots$
Suppose some interpretation $v$ assigns $T$ to $p$.
Then $v \left({\neg p}\right) = F$
So:
: $v \left({\cdots \circ \left({p \circ p}\right) \circ \cdots}\right) = F$
So it has to be true that $T \circ T = F$, otherwise:
: $v \left({\cdots \circ \left({T \circ T}\right) \circ \cdots}\right) = v \left({\cdots \circ \left({T}\right) \circ \cdots}\right) = T$
Similarly:
:$F \circ F = T$
Now consider $T \circ F$ and $F \circ T$.
Suppose $T \circ F = F$.
If $F \circ T = T$, then we have the function defined by this truth table:
{| border="1" cellpadding="4" cellspacing="1" style="text-align:center;"
|- 
! $v \left({p}\right)$
! $v \left({q}\right)$
! $v \left({p \circ q}\right)$
|-
| $F$ || $F$ || $T$
|-
| $F$ || $T$ || $T$
|-
| $T$ || $F$ || $F$
|-
| $T$ || $T$ || $F$
|}
which is $\neg p$, and hence only negation would be definable.
So if $T \circ F = F$ we need $F \circ T = F$.
This gives the truth table for the NOR function:
{| border="1" cellpadding="4" cellspacing="1" style="text-align:center;"
|- 
! $v \left({p}\right)$
! $v \left({q}\right)$
! $v \left({p \circ q}\right)$
|-
| $F$ || $F$ || $T$
|-
| $F$ || $T$ || $F$
|-
| $T$ || $F$ || $F$
|-
| $T$ || $T$ || $F$
|}
... which we have seen is functionally complete.
Similarly, Suppose $T \circ F = T$.
If $F \circ T = F$, then we have the function defined by this truth table:
{| border="1" cellpadding="4" cellspacing="1" style="text-align:center;"
|- 
! $v \left({p}\right)$
! $v \left({q}\right)$
! $v \left({p \circ q}\right)$
|-
| $F$ || $F$ || $T$
|-
| $F$ || $T$ || $F$
|-
| $T$ || $F$ || $T$
|-
| $T$ || $T$ || $F$
|}
which is $\neg q$, and hence only negation would be definable.
So if $T \circ F = T$ we need $F \circ T = T$.
This gives the truth table for the NAND function:
{| border="1" cellpadding="4" cellspacing="1" style="text-align:center;"
|- 
! $v \left({p}\right)$
! $v \left({q}\right)$
! $v \left({p \circ q}\right)$
|-
| $F$ || $F$ || $T$
|-
| $F$ || $T$ || $T$
|-
| $T$ || $F$ || $T$
|-
| $T$ || $T$ || $F$
|}
... which we have seen is functionally complete.
Thus it follows that there can be no functionally complete binary logical connectives apart from NAND and NOR.
{{qed}}
Theorem: Conditional and Converse are not Equivalent

A conditional statement:
:$p \implies q$
is not logically equivalent to its converse:
:$q \implies p$

Proof:
We apply the Method of Truth Tables to the proposition:
:$\paren {p \implies q} \iff \paren {q \implies p}$
$\begin{array}{|ccc|c|ccc|} \hline
p & \implies & q) & \iff & (q & \implies & p) \\
\hline
\F & \T & \F & \T & \F & \T & \F \\
\F & \T & \T & \F & \T & \F & \F \\
\T & \F & \F & \F & \F & \T & \T \\
\T & \T & \T & \T & \T & \T & \T \\
\hline
\end{array}$
As can be seen by inspection, the truth values under the main connectives do not match for all boolean interpretations.
{{qed}}
Theorem: De Morgan's Laws (Predicate Logic)/Assertion of Universality

:$\forall x: \map P x \dashv \vdash \neg \paren {\exists x: \neg \map P x}$
::''If everything '''is''', there exists nothing that '''is not'''.''

Proof:
{{BeginTableau|\forall x: \map P x \vdash \neg \paren {\exists x: \neg \map P x} }}
{{Premise|1|\forall x: \map P x}}
{{Assumption|2|\exists x: \neg \map P x}}
{{TableauLine|n = 3|pool = 2|f = \neg \map P {\mathbf a}|rlnk = Existential Instantiation|rtxt = Existential Instantiation|dep = 2|c = for some arbitrary $\mathbf a$}}
{{TableauLine|n = 4|pool = 1|f = \map P {\mathbf a}|rlnk = Universal Instantiation|rtxt = Universal Instantiation|dep = 1}}
{{NonContradiction|5|1, 2|3|4}}
{{Contradiction|6|1|\neg \paren {\exists x: \neg \map P x}|2|5}}
{{EndTableau|lemma}}
{{BeginTableau|\neg \paren {\exists x: \neg \map P x} \vdash \forall x: \map P x}}
{{Premise|1|\neg \paren {\exists x: \neg \map P x} }}
{{Assumption|2|\neg \paren {\forall x: \map P x} }}
{{SequentIntro|3|2|\exists x: \neg \map P x|2|Denial of Universality}}
{{NonContradiction|4|1, 2|1|3}}
{{Reductio|5|1|\forall x: \map P x|2|4}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum}}
{{Namedfor|Augustus De Morgan|cat = De Morgan}}
Theorem: De Morgan's Laws (Predicate Logic)/Denial of Existence

:$\forall x: \neg \map P x \dashv \vdash \neg \paren {\exists x: \map P x}$
::''If everything '''is not''', there exists nothing that '''is'''.''

Proof:
{{BeginTableau|\forall x: \neg \map P x \vdash \neg \paren {\exists x: \map P x} }}
{{Premise|1|\forall x: \neg \map P x}}
{{Assumption|2|\exists x: \map P x}}
{{TableauLine|n = 3|pool = 2|f = \map P {\mathbf a}|rlnk = Existential Instantiation|rtxt = Existential Instantiation|dep = 2|c = for an arbitrary $\mathbf a$}}
{{TableauLine|n = 4|pool = 1|f = \neg \map P {\mathbf a}|rlnk = Universal Instantiation|rtxt = Universal Instantiation|dep = 3}}
{{NonContradiction|5|1, 2|3|4}}
{{Contradiction|6|1|\neg \paren {\exists x: \map P x}|2|5}}
{{EndTableau|lemma}}
{{BeginTableau|\neg \paren {\exists x: \map P x} \vdash \forall x: \neg \map P x}}
{{Premise|1|\neg \paren {\exists x: \map P x} }}
{{Assumption|2|\map P {\mathbf a}|for some arbitrary $\mathbf a$}}
{{TableauLine|n = 3|pool = 2|f = \exists x: \map P x|rlnk = Existential Generalisation|rtxt = Existential Generalisation|dep = 2}}
{{NonContradiction|4|1, 2|1|3}}
{{Contradiction|5|1|\neg \map P {\mathbf a}|2|4}}
{{TableauLine|n = 6|pool = 1|f = \forall x: \neg \map P x|rlnk = Universal Generalisation|rtxt = Universal Generalisation|dep = 5|c = as $\mathbf a$ was arbitrary}}
{{EndTableau|qed}}
{{Namedfor|Augustus De Morgan|cat = De Morgan}}
Theorem: De Morgan's Laws (Predicate Logic)/Assertion of Existence

:$\neg \paren {\forall x: \neg \map P x} \dashv \vdash \exists x: \map P x$
::''If not everything '''is not''', there exists something that '''is'''.''

Proof:
{{BeginTableau|\neg \paren {\forall x: \neg \map P x} \vdash \exists x: \map P x}}
{{Premise|1|\neg \paren {\forall x: \neg \map P x} }}
{{Assumption|2|\neg \paren {\exists x: \map P x} }}
{{SequentIntro|3|2|\forall x: \neg \map P x|2|Denial of Existence}}
{{NonContradiction|4|1, 2|1|3}}
{{Reductio|5|1|\exists x: \map P x|2|4}}
{{EndTableau|lemma}}
{{BeginTableau|\exists x: \map P x \vdash \neg \paren {\forall x: \neg \map P x} }}
{{Premise|1|\exists x: \map P x}}
{{Assumption|2|\forall x: \neg \map P x}}
{{TableauLine|n = 3|pool = 1|f = \map P {\mathbf a}|rlnk = Existential Instantiation|rtxt = Existential Instantiation|dep = 1|for some arbitrary $\mathbf a$}}
{{TableauLine|n = 4|pool = 2|f = \neg \map P {\mathbf a}|rlnk = Universal Instantiation|rtxt = Universal Instantiation|dep = 2}}
{{NonContradiction|5|1, 2|3|4}}
{{Contradiction|6|1|\neg \paren {\forall x: \neg \map P x}|2|5}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum}}
{{Namedfor|Augustus De Morgan|cat = De Morgan}}
Theorem: Conjunction in terms of NAND

:$p \land q \dashv \vdash \paren {p \uparrow q} \uparrow \paren {p \uparrow q}$
where $\land$ denotes logical conjunction and $\uparrow$ denotes logical NAND.

Proof:
{{begin-eqn}}
{{eqn | l = p \land q
      | o = \dashv \vdash
      | r = \neg \neg \paren {p \land q}
      | c = Double Negation
}}
{{eqn | o = \dashv \vdash
      | r = \neg \paren {p \uparrow q}
      | c = {{Defof|Logical NAND}}
}}
{{eqn | o = \dashv \vdash
      | r = \paren {p \uparrow q} \uparrow \paren {p \uparrow q}
      | c = NAND with Equal Arguments
}}
{{end-eqn}}
{{qed}}
Theorem: Disjunction in terms of NOR

:$p \lor q \dashv \vdash \paren {p \downarrow q} \downarrow \paren {p \downarrow q}$
where $\lor$ denotes logical disjunction and $\downarrow$ denotes logical NOR.

Proof:
{{begin-eqn}}
{{eqn | l = p \lor q
      | o = \dashv \vdash
      | r = \neg \neg \paren {p \lor q}
      | c = Double Negation
}}
{{eqn | o = \dashv \vdash
      | r = \neg \paren {p \downarrow q}
      | c = {{Defof|Logical NOR}}
}}
{{eqn | o = \dashv \vdash
      | r = \paren {p \downarrow q} \downarrow \paren {p \downarrow q}
      | c = NOR with Equal Arguments
}}
{{end-eqn}}
{{qed}}
Category:Logical NOR
Category:Disjunction
4dw5e72qt5juo7ko2pxvsrci6p0nyyc
Theorem: Disjunction in terms of NAND

:$p \lor q \dashv \vdash \paren {p \uparrow p} \uparrow \paren {q \uparrow q}$
where $\lor$ denotes logical disjunction and $\uparrow$ denotes logical NAND.

Proof:
{{begin-eqn}}
{{eqn | l = p \lor q
      | o = \dashv \vdash
      | r = \neg \paren {\neg p \land \neg q}
      | c = De Morgan's Laws (Logic): Disjunction
}}
{{eqn | o = \dashv \vdash
      | r = \neg p \uparrow \neg q
      | c = {{Defof|Logical NAND}}
}}
{{eqn | o = \dashv \vdash
      | r = \paren {p \uparrow p} \uparrow \paren {q \uparrow q}
      | c = NAND with Equal Arguments
}}
{{end-eqn}}
{{qed}}
Theorem: Conditional in terms of NAND

:$p \implies q \dashv \vdash p \uparrow \paren {q \uparrow q}$

Proof:
{{begin-eqn}}
{{eqn | l = p \implies q
      | o = \dashv \vdash
      | r = \neg \paren {p \land \neg q}
      | c = Conditional is Equivalent to Negation of Conjunction with Negative
}}
{{eqn | o = \dashv \vdash
      | r = p \uparrow \neg q
      | c = {{Defof|Logical NAND}}
}}
{{eqn | o = \dashv \vdash
      | r = p \uparrow \paren {q \uparrow q}
      | c = NAND with Equal Arguments
}}
{{end-eqn}}
{{qed}}
Theorem: Conditional in terms of NAND

:$p \implies q \dashv \vdash p \uparrow \paren {q \uparrow q}$

Proof:
{{begin-eqn}}
{{eqn | l = p \implies q
      | o = \dashv \vdash
      | r = \neg p \lor q
      | c = Rule of Material Implication
}}
{{eqn | o = \dashv \vdash
      | r = \neg p \lor \neg \neg q
      | c = Double Negation Introduction
}}
{{eqn | o = \dashv \vdash
      | r = p \uparrow \neg q
      | c = NAND as Disjunction of Negations
}}
{{eqn | o = \dashv \vdash
      | r = p \uparrow \left({q \uparrow q}\right)
      | c = NAND with Equal Arguments
}}
{{end-eqn}}
{{qed}}
Theorem: Biconditional in terms of NAND

:$p \iff q \dashv \vdash \paren {\paren {p \uparrow p} \uparrow \paren {q \uparrow q} } \uparrow \paren {p \uparrow q}$
where $\iff$ denotes logical biconditional and $\uparrow$ denotes logical NAND.

Proof:
{{begin-eqn}}
{{eqn | l = p \iff q
      | o = \dashv \vdash
      | r = \neg \paren {p \oplus q}
      | c = Exclusive Or is Negation of Biconditional
}}
{{eqn | o = \dashv \vdash
      | r = \neg \paren {\paren {p \lor q} \land \neg \paren {p \land q} }
      | c = {{Defof|Exclusive Or}}
}}
{{eqn | o = \dashv \vdash
      | r = \neg \paren {\paren {p \lor q} \land \paren {p \uparrow q} }
      | c = {{Defof|Logical NAND}}
}}
{{eqn | o = \dashv \vdash
      | r = \neg \paren {\paren {\paren {p \uparrow p} \uparrow \paren {q \uparrow q} } \land \paren {p \uparrow q} }
      | c = Disjunction in terms of NAND
}}
{{eqn | o = \dashv \vdash
      | r = \paren {\paren {p \uparrow p} \uparrow \paren {q \uparrow q} } \uparrow \paren {p \uparrow q}
      | c = {{Defof|Logical NAND}}
}}
{{end-eqn}}
{{qed}}
Theorem: Mapping is Injection and Surjection iff Inverse is Mapping

Let $f: S \to T$ be a mapping.
Then:
: $f: S \to T$ can be defined as a bijection in the sense that:
::$(1): \quad f$ is an injection
::$(2): \quad f$ is a surjection
{{iff}}:
:the inverse $f^{-1}$ of $f$ is itself a mapping.

Proof:
=== Necessary Condition ===
{{:Inverse of Injective and Surjective Mapping is Mapping}}
Theorem: Mapping is Injection and Surjection iff Inverse is Mapping

Let $f: S \to T$ be a mapping.
Then:
: $f: S \to T$ can be defined as a bijection in the sense that:
::$(1): \quad f$ is an injection
::$(2): \quad f$ is a surjection
{{iff}}:
:the inverse $f^{-1}$ of $f$ is itself a mapping.

Proof:
=== Necessary Condition ===
{{:Inverse of Injective and Surjective Mapping is Mapping/Proof 2}}{{qed|lemma}}
=== Sufficient Condition ===
Let $f^{-1}: T \to S$ be a mapping.
By Inverse Mapping is Bijection, both $f$ and $f^{-1}$ are bijections.
Hence, in particular, $f$ is a bijection.
{{qed}}
Theorem: Condition for Composite Mapping to be Identity

Let $S$ and $T$ be sets.
Let $f: S \to T$ and $g: T \to S$ be mappings such that:
: $g \circ f = I_S$
where $I_S$ is the identity mapping on $S$.
Then $f$ is an injection and $g$ is a surjection.

Proof:
From Identity Mapping is Bijection, $I_S$ is a bijection.
From Identity Mapping is Injection, $I_S$ is an injection.
From Injection if Composite is Injection it follows that $f$ is an injection.
From Identity Mapping is Surjection, $I_S$ is a surjection.
From Surjection if Composite is Surjection it follows that $g$ is a surjection.
{{qed}}
Theorem: Bijection iff exists Mapping which is Left and Right Inverse

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a mapping.
Then $f$ is a bijection {{iff}}:
:there exists a mapping $g: T \to S$ such that:
::$g \circ f = I_S$
::$f \circ g = I_T$
:where $I_S$ and $I_T$ are the identity mappings on $S$ and $T$ respectively.

Proof:
=== Necessary Condition ===
Let $f$ be a bijection.
Then for each $y \in T$ there exists one and only one $x \in S$ such that $\map f x = y$.
That is, that there exists a mapping $g: T \to S$ with the property that:
: $\forall y \in T: \exists x \in S: \map g y = x$
Let $y \in T$.
Let $x = g \map g y$.
Then:
{{begin-eqn}}
{{eqn | l = y
      | r = \map f {\map g y}
      | c = 
}}
{{eqn | r = \map {f \circ g} y
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = x
      | r = \map g {\map f x}
      | c = 
}}
{{eqn | r = \map {f \circ g} x
      | c = 
}}
{{end-eqn}}
demonstrating that $g$ has the property that:
:$g \circ f = I_S$
:$f \circ g = I_T$
{{qed|lemma}}
Theorem: Eigenvalues of G-Representation are Roots of Unity

Let $G$ be a finite group.
Let $\left({K, +, \cdot}\right)$ be a field.
Let $V$ be a $G$-module over $K$ (i.e. $V$ is a $K \left[{G}\right]$-module).
Then $\forall g \in G$, the eigenvalues of the action by the vector $g \in K \left[{G}\right]$ on $V$ are roots of unity.

Proof:
Fix an arbitrary $g \in G$ and consider the corresponding vector $g \in K \left[{G}\right]$.
Let $\lambda$ be an eigenvalue of $g$, that is $\lambda$ is an eigenvalue of the map in $\operatorname{Aut} \left({V}\right): \vec v \mapsto g \vec v$.
Then by definition of an eigenvalue we have:
:$\exists \vec v_\lambda \in V : g \vec v_\lambda = \lambda \vec v_\lambda$
Let $n$ be the order of $g$ in $G$.
Then:
{{begin-eqn}}
{{eqn | l = \vec v_\lambda
      | r = g^n \vec v_\lambda
      | c = as $g^n = e$ and $e$ acts trivially on $V$
}}
{{eqn | r = \lambda g^{n-1} \vec v_\lambda
      | c = as $G$ acts linearly on $V$
}}
{{eqn | r = \vdots
      | c = Continue exchanging $g^k \vec v_\lambda$ with $\lambda g^{k-1} \vec v_\lambda$
}}
{{eqn | r = \lambda^n \vec v_\lambda
      | c = as $g^0 = e$ which acts trivially on $V$
}}
{{end-eqn}}
{{explain|"as $g^n {{=}} e$ and $e$ acts trivially on $V$" - this needs to be linked to and / or proved}}
{{explain|"as $G$ acts linearly on $V$" - this needs to be linked to and / or proved}}
{{explain|"as $g^0 = e$ which acts trivially on $V$" - this needs to be linked to and / or proved}}
Thus:
:$\vec v_\lambda = \lambda^n \vec v_\lambda$
which means:
:$\lambda^n = 1$
and thus by definition, $\lambda$ is an $n$th root of unity.
{{qed}}
la77w1qnzjsm0z4avytxiwx9t7fuetp
Theorem: Character of Representations over C are Algebraic Integers

Let $G$ be a finite group.
Let $\chi$ be the character of any $\C \sqbrk G$-module $\struct {V, \rho}$.
Then for all $g \in G$, it follows that $\map \chi g$ is an algebraic integer.

Proof:
By the definition of character:
:$\map \chi g = \map \tr {\rho_g}$
where $\map \tr {\rho_g}$ is the trace of $\rho_g$.
{{explain|$\rho_g$}}
where:
:$\rho \in \map \hom {\C \sqbrk G, \Aut V}: \vec {e_g} \mapsto \rho_g$
by definition.
{{explain|The above definition is not stated in that form on {{ProofWiki}}. Link to $\map \hom {\C \sqbrk G, \Aut V}$, clarify specifically what $\C \sqbrk G$ is, and define $\vec {e_g}$.}}
Fix an arbitrary $g \in G$.
Let $\order g$ denote the order of $g$.
The trace $\map \tr {\rho_g}$ of $\rho_g$ is defined as the sum of the eigenvalues of $\rho_g$.
{{explain|The definition of Trace needs to be reviewed.}}
From Eigenvalues of G-Representation are Roots of Unity, we have that any eigenvalue $\lambda$ of $\rho_g$ is a root of unity whose order is $\order g$.
We have that $\lambda$ satisfies the monic polynomial $x^{\order g} - 1$
Hence we have that $\lambda$ is an algebraic integer.
From Ring of Algebraic Integers, we have that the sum of the eigenvalues is also an algebraic integer.
Thus $\map \chi g$ is an algebraic integer.
{{qed}}
Category:Module Theory
Category:Group Theory
Category:Complex Analysis
d9l0wf1rw67chqmlhzctsow4pvolao6
Theorem: Injection from Finite Set to Itself is Surjection

Let $S$ be a finite set.
Let $f: S \to S$ be an injection.
Then $f$ is also a surjection.

Proof:
Let $a \in S$.
We need to show that there exists $b \in S$ such that $a = \map f b$.
Consider what happens when $f$ is applied repeatedly on $S$.
Let $f^2$ denote $f \circ f$ and, generally, $f^n := f \circ f^{n-1}$.
Consider the sequence of elements of $S$:
:$a, \map f a, \map {f^2} a, \ldots$
Because $S$ is a finite set, there must be repetitions.
That is, there must exist $r, s \in \N$ such that:
:$\map {f^r} a = \map {f^s} a$
where $r \ne s$.
{{WLOG}}, assume $r > s$.
$f$ is an injection.
Therefore by Composite of Injections is Injection, $f^s$ is an injection.
By Injection iff Left Cancellable, $f^s$ is left cancellable.
Thus:
{{begin-eqn}}
{{eqn | l = \map {f^r} a
      | r = \map {f^s} a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {f^s \circ f^{r - s} } a
      | r = \map {f^s} a
}}
{{eqn | ll= \leadsto
      | l = \map {f^{r - s} } a
      | r = a
      | c = {{Defof|Left Cancellable Mapping}}
}}
{{end-eqn}}
That is, $b = \map {f^{r - s - 1} } a$.
{{qed}}
Theorem: Codomain of Bijection is Domain of Inverse

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a bijection.
Let $f^{-1}: T \to S$ be the inverse of $f$.
Then the domain of $f^{-1}$ equals the codomain of $f$.

Proof:
Follows directly from the definition of domain and codomain:
:$\Dom f = S$ and $\Cdm f = T$
:$\Dom {f^{-1} } = T$ and $\Cdm {f^{-1} } = S$
That is:
:$\Dom {f^{-1} } = T = \Cdm f$
{{qed}}
Theorem: Domain of Bijection is Codomain of Inverse

Let $S$ and $T$ be sets.
Let $f: S \to T$ be a bijection.
Let $f^{-1}: T \to S$ be the inverse of $f$.
Then the codomain of $f^{-1}$ equals the domain of $f$.

Proof:
Follows directly from the definition of domain and codomain:
:$\Dom f = S$ and $\Cdm f = T$
:$\Dom {f^{-1} } = T$ and $\Cdm {f^{-1} } = S$
That is:
:$\Cdm {f^{-1} } = S = \Dom f$
{{qed}}
Theorem: Conditions for Uniqueness of Left Inverse Mapping

Let $S$ and $T$ be sets such that $S \ne \O$.
Let $f: S \to T$ be an injection.
Then a left inverse mapping of $f$ is in general not unique.
Uniqueness occurs under either of two circumstances:
:$(1): \quad S$ is a singleton
:$(2): \quad f$ is a bijection.

Proof:
If $f$ is a bijection, then by definition $f$ is also a surjection.
Then:
:$T \setminus \Img f = \O$
:and we have that $g = f^{-1}$.
As $f^{-1}$ is uniquely defined $g$ is itself unique.
{{qed|lemma}}
If $S$ is a singleton then there can only be one mapping $g: T \to S$:
:$\forall t \in T: \map g t = s$
{{qed|lemma}}
If $f$ is not a bijection, then as it is an injection it can not be a surjection.
Then:
:$T \setminus \Img f \ne \O$
Let $t \in T \setminus \Img f$.
We can now choose any $x_0 \in S$ such that $\map g t = x_0$.
If $S$ is not a singleton, such an $x_0$ is not unique.
Hence the result.
{{qed}}