avewright/proofwiki-math huggingface dataset:
Theorem: Spectral Theorem for Unitary Matrices

Let $\mathbf A$ be a square matrix.
Then, $\mathbf A$ is a unitary matrix {{Iff}} it is diagonalizable via a unitary transformation to a diagonal matrix whose diagonal elements are of unit modulus.
That is, we can write:
:$\mathbf A = \mathbf U \mathbf D \mathbf U^\dagger$
where
:$\mathbf U$ is a unitary matrix
:$\mathbf D$ is a diagonal matrix whose diagonal elements are of unit modulus
:$\mathbf U^\dagger$ is the Hermitian conjugate of $\mathbf U$

Proof:
=== Necessary Case ===
Let $A$ be diagonalizable via a unitary transformation to a diagonal matrix whose diagonal elements are of unit modulus.
Let $d_i = \sqbrk {\mathbf D}_{ii}$ be the $i^{th}$ diagonal element of $\mathbf D$.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf A^{-1}
      | r = \paren {\mathbf U \mathbf D \mathbf U^\dagger}^{-1}
}}
{{eqn | r = \paren {\mathbf U^\dagger}^{-1} \mathbf D^{-1} \mathbf U^{-1}
      | c = Inverse of Matrix Product
}}
{{eqn | r = \mathbf U \mathbf D^{-1} \mathbf U^\dagger
      | c = {{Defof|Unitary Matrix}}
}}
{{eqn | r = \mathbf U \overline {\mathbf D} \mathbf U^\dagger
      | c = Inverse of Diagonal Matrix and Reciprocal of Complex Number and $\size {d_i} = 1$
}}
{{eqn | r = \mathbf U \mathbf D^\dagger \mathbf U^\dagger
      | c = {{Defof|Hermitian Conjugate}}
}}
{{eqn | r = \paren {\mathbf U \mathbf D \mathbf U^\dagger}^\dagger
      | c = Hermitian Conjugate of Matrix Product
}}
{{eqn | r = \mathbf A^\dagger
}}
{{end-eqn}}
Therefore, $\mathbf A$ is unitary.
{{qed|lemma}}
Theorem: Eigenvalues of Anti-Hermitian Matrix are Imaginary

The eigenvalues of an anti-Hermitian matrix are imaginary.

Proof:
Let $\mathbf H$ be an anti-Hermitian matrix.
Let $\lambda$ be an eigenvalue of $\mathbf H$.
Let $\mathbf v$ be a eigenvector of $\mathbf H$ associated with $\lambda$.
Then:
{{begin-eqn}}
{{eqn | l = \lambda \innerprod {\mathbf v} {\mathbf v}
      | r = \innerprod {\lambda \mathbf v} {\mathbf v}
      | c = Inner Product is Sesquilinear
}}
{{eqn | r = \innerprod {\mathbf H \mathbf v} {\mathbf v}
      | c = {{Defof|Eigenvector}} and {{Defof|Eigenvalue}}
}}
{{eqn | r = \innerprod {\mathbf v} {\mathbf H^* \mathbf v}
      | c = {{Defof|Adjoint Operator}}
}}
{{eqn | r = \innerprod {\mathbf v} {\mathbf H^\dagger \mathbf v}
      | c = Hermitian Conjugate is Adjoint
}}
{{eqn | r = \innerprod {\mathbf v} {-\mathbf H \mathbf v}
      | c = {{Defof|Anti-Hermitian Matrix}}
}}
{{eqn | r = \innerprod {\mathbf v} {-\lambda \mathbf v}
      | c = {{Defof|Eigenvector}} and {{Defof|Eigenvalue}}
}}
{{eqn | r = -\overline \lambda \innerprod {\mathbf v} {\mathbf v}
      | c = Inner Product is Sesquilinear
}}
{{end-eqn}}
Thus, we have:
:$\lambda \innerprod {\mathbf v} {\mathbf v} = -\overline \lambda \innerprod {\mathbf v} {\mathbf v}$
Since $\mathbf v$ is an eigenvector, it cannot be a zero vector.
So, $\innerprod {\mathbf v} {\mathbf v} > 0$ as required of an inner product.
Dividing by $\innerprod {\mathbf v} {\mathbf v}$ gives:
:$\lambda = -\overline \lambda$
From Complex Number equals Negative of Conjugate iff Wholly Imaginary, $\lambda$ is imaginary.
{{qed}}
Category:Anti-Hermitian Matrices
Category:Eigenvalues of Square Matrices
0x2fs850wlmpenayv2qf9pui1rhu7lx
Theorem: Spectral Theorem for Anti-Hermitian Matrices

Let $\mathbf A$ be a square matrix over $\mathbb C$.
Then $\mathbf A$ is anti-Hermitian {{Iff}} it is diagonalizable to an imaginary diagonal matrix via a unitary transformation.
That is, we can write:
:$\mathbf A = \mathbf U \mathbf D \mathbf U^\dagger$
where:
:$\mathbf D$ is an imaginary diagonal matrix
:$\mathbf U$ is a unitary matrix
:$\mathbf U^\dagger$ is the Hermitian conjugate of $\mathbf U$.

Proof:
=== Necessary Case ===
Let $\mathbf A$ be diagonalizable to a imaginary diagonal matrix via a unitary transformation.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf A^\dagger
      | r = \paren {\mathbf U \mathbf D \mathbf U^\dagger}^\dagger
}}
{{eqn | r = \mathbf U \mathbf D^\dagger \mathbf U^\dagger
      | c = Hermitian Conjugate of Matrix Product and Hermitian Conjugate is Involution
}}
{{eqn | r = \mathbf U \paren {-\mathbf D} \mathbf U^\dagger
      | c = $\mathbf D$ is imaginary and diagonal
}}
{{eqn | r = -\mathbf U \mathbf D \mathbf U^\dagger
      | c = Matrix Multiplication is Homogeneous of Degree 1
}}
{{eqn | r = -\mathbf A
}}
{{end-eqn}}
Therefore, $\mathbf A$ is anti-Hermitian.
{{qed|lemma}}
Theorem: Real Anti-Symmetric Matrix is Anti-Hermitian

A real anti-symmetric matrix is anti-Hermitian.

Proof:
Let $\mathbf A$ be a real anti-symmetric matrix.
Then:
{{begin-eqn}}
{{eqn | l = \mathbf A^\dagger
      | r = \mathbf A^\intercal
      | c = $\mathbf A$ is real
}}
{{eqn | r = -\mathbf A
      | c = {{Defof|Anti-Symmetric Matrix}}
}}
{{end-eqn}}
Therefore, $\mathbf A$ is anti-Hermitian.
{{qed}}
Category:Antisymmetric Matrices
Category:Anti-Hermitian Matrices
Category:Real Matrices
d0ihvfauxj87p6ejmdfb191y0h3iyqi
Theorem: Eigenvalues of Real Anti-Symmetric Matrix are Imaginary

The eigenvalues of a real anti-symmetric matrix are imaginary.

Proof:
Follows directly from Real Anti-Symmetric Matrix is Anti-Hermitian and Eigenvalues of Anti-Hermitian Matrix are Imaginary.
{{qed}}
Category:Real Matrices
Category:Antisymmetric Matrices
Category:Anti-Hermitian Matrices
Category:Eigenvalues of Square Matrices
Category:Eigenvalues of Real Square Matrices
d2d60pq8lcwy5wh6yqlt44eb57518xj
Theorem: Spectral Theorem for Real Anti-Symmetric Matrices

Let $\mathbf A$ be a square matrix over $\R$.
Then $\mathbf A$ is anti-symmetric {{Iff}} it is diagonalizable to an imaginary diagonal matrix via a unitary transformation.
That is, we can write:
:$\mathbf A = \mathbf U \mathbf D \mathbf U^\dagger$
where:
:$\mathbf D$ is an imaginary diagonal matrix
:$\mathbf U$ is a unitary matrix
:$\mathbf U^\dagger$ is the Hermitian conjugate of $\mathbf U$.

Proof:
=== Necessary Case ===
Let $\mathbf A$ be diagonalizable to an imaginary diagonal matrix via a unitary transformation.
From Spectral Theorem for Anti-Hermitian Matrices, $\mathbf A$ is anti-Hermitian.
Thus:
:$\mathbf A^\dagger = -\mathbf A$
Since $\mathbf A$ is real, $\mathbf A^\dagger = \mathbf A^\intercal$.
Thus:
:$\mathbf A^\intercal = -\mathbf A$
So, $\mathbf A$ is anti-symmetric.
{{qed|lemma}}
Theorem: Eigenvalues of Real Orthogonal Matrix have Unit Modulus and occur in Conjugate Pairs

Let $\mathbf R$ be a real orthogonal matrix.
Let $\lambda$ be an eigenvalue of $\mathbf R$.
Then:
:$\size \lambda = 1$
and
:$\overline \lambda$ is also an eigenvalue

Proof:
From Real Orthogonal Matrix is Unitary, $\mathbf R$ is unitary.
From Eigenvalues of Unitary Matrix have Unit Modulus:
:$\size \lambda = 1$
We have that $\mathbf R$ is real.
From Complex Eigenvalues of Real Matrix occur in Conjugate Pairs, $\overline {\mathbf \lambda}$ is also an eigenvalue.
{{qed}}
Category:Orthogonal Matrices
Category:Eigenvalues of Square Matrices
Category:Eigenvalues of Real Square Matrices
sfgpi1738bj6lu994o761r7rgjjk8zl
Theorem: Spectral Theorem for Real Orthogonal Matrices

Let $\mathbf A$ be a square matrix over $\R$.
Then, $\mathbf A$ is orthogonal {{Iff}} it is diagonalizable via a unitary transformation to a diagonal matrix whose diagonal elements are of unit modulus which occur in conjugate pairs.
That is, we can write:
:$\mathbf A = \mathbf U \mathbf D \mathbf U^\dagger$
where
:$\mathbf U$ is a unitary matrix
:$\mathbf D$ is a diagonal matrix whose diagonal elements are of unit modulus which occur in conjugate pairs
:$\mathbf U^\dagger$ is the Hermitian conjugate of $\mathbf U$

Proof:
=== Necessary Case ===
Let $\mathbf A$ be a real matrix that is diagonalizable via a unitary transformation to a diagonal matrix whose diagonal elements are of unit modulus which occur in conjugate pairs.
From Spectral Theorem for Unitary Matrices, $\mathbf A$ is unitary.
Since $\mathbf A$ is real:
{{begin-eqn}}
{{eqn | l = \mathbf A^\intercal
      | r = \mathbf A^\dagger
      | c = Hermitian Conjugate of Real Matrix is Transpose
}}
{{eqn | r = \mathbf A^{-1}
      | c = {{Defof|Unitary Matrix}}
}}
{{end-eqn}}
Thus, $\mathbf A$ is a orthogonal.
{{qed|lemma}}
Theorem: Complex Eigenvalues of Real Matrix occur in Conjugate Pairs

The complex eigenvalues of a real matrix occur in conjugate pairs.
That is, if $\lambda$ is a complex eigenvalues of a real matrix, then so is the complex conjugate $\overline \lambda$.

Proof:
By definition, the eigenvalues of a matrix are the roots of its characteristic polynomial.
The characteristic polynomial of a real matrix has real coefficients.
From Complex Roots of Polynomial with Real Coefficients occur in Conjugate Pairs, the complex eigenvalues come in conjugate pairs.
{{qed}}
Category:Eigenvalues of Square Matrices
Category:Real Matrices
88a59q9yqlpgva7s2k0dxlj2fk14lh5
Theorem: Expected Number of Rolls until Two Consecutive Heads

Let $0 < p \le 1$.
Consider a coin such that we toss a head with probability $p$.
We repeatedly toss this coin until we observe two consecutive heads.
The expected number of tosses until we observe two consecutive heads is:
:$\ds \frac 1 p + \frac 1 {p^2}$

Proof:
Let $E$ be the expected number of tosses until we observe two consecutive heads.
Let $E_H$ be the expected number of further tosses until we observe two consecutive heads given that our previous toss is a head.
Let $q = 1 - p$. 
By the Total Expectation Theorem, we have:
:$E = p \expect {\text {number of tosses until two consecutive heads} \mid \text {first toss is a head} } + q \expect {\text {number of tosses until two consecutive heads} \mid \text {first toss is a tails} }$
Given that the first toss is a heads, we have $1$ toss until the first head, and then in expectation $E_H$ further tosses until observing two consecutive heads.
Hence:
:$\expect {\text {number of tosses until two consecutive heads} \mid \text {first toss is a head} } = 1 + E_H$
Given that the first toss is a tail, we add $1$ to the tally of tosses and restart the simulation. 
Hence:
:$\expect {\text {number of tosses until two consecutive heads} \mid \text {first toss is a tails} } = 1 + E$
Applying the Total Expectation Theorem again, we have:
{{begin-eqn}}
{{eqn	| l = E_H
		| r = p \expect {\text {number of further tosses until two consecutive heads} \mid \text {we have already seen a head and next toss is a head} }
}}
{{eqn	| o = +
		| r = q \expect {\text {number of further tosses until two consecutive heads} \mid \text {we have already seen a head and next toss is a tail} }
}}
{{end-eqn}}
In the first case, since our next toss is a head:
:$\expect {\text {number of further tosses until two consecutive heads} \mid \text {we have already seen a head and next toss is a head} } = 1$
In the second case, we restart the simulation with an extra toss on the tally (from the tail), and so:
:$\expect {\text {number of further tosses until two consecutive heads} \mid \text {we have already seen a head and next toss is a tail} } = 1 + E$
We now have the system of equations:
:$(1): \quad E = p \paren {1 + E_H} + q \paren {1 + E}$
:$(2): \quad E_H = p + q \paren {1 + E}$
Since $p + q = 1$, we have:
:$(1): \quad E = 1 + p E_H + q E$
:$(2): \quad E_H = 1 + q E$
Substituting $(2)$ into $(1)$, we obtain:
:$E = 1 + p \paren {1 + q E} + q E$
and so:
:$E = 1 + p + \paren {p q + q} E$
We can rearrange this to:
:$E = \dfrac {1 + p} {1 - p q - q}$
We can then write:
{{begin-eqn}}
{{eqn	| l = 1 - p q - q
		| r = 1 - p \paren {1 - p} - \paren {1 - p}
}}
{{eqn	| r = 1 - p + p^2 - 1 + p
}}
{{eqn	| r = p^2 
}}
{{end-eqn}}
We therefore have:
:$E = \dfrac {1 + p} {p^2} = \dfrac 1 p + \dfrac 1 {p^2}$
{{qed}}
Category:Combinatorics
Category:Coins
3q9sg22nqpk5rmq1x8wuq472hm8uf8z
Theorem: Probability that Uniformly Selected Subset contains Particular Element

Let $X$ be a finite set.
Let $\powerset X$ be the power set of $X$.
Give $\powerset X$ the discrete uniform distribution, so that:
:$\ds \map \Pr {\set A} = 2^{-n}$ for each $A \in \powerset X$.
Let $x \in X$.
Then:
:$\ds \map \Pr {\set {A \in \powerset X : x \in A} } = \frac 1 2$

Proof:
We count the cardinality of $\set {A \in \powerset X : x \in A}$.
All sets $C \in \set {A \in \powerset X : x \in A}$ can be written uniquely in the form $\set x \cup B$, where $B \in \powerset {A \setminus \set x}$.
In particular, $B = C \setminus \set x$. 
From Cardinality of Power Set of Finite Set, we have $\card {\powerset {A \setminus \set x} } = 2^{n - 1}$.
Hence the cardinality of $\set {A \in \powerset X : x \in A}$ is $2^{n - 1}$.
So, from the definition of the discrete uniform distribution:
:$\ds \map \Pr {\set {A \in \powerset X : x \in A} } = \frac {2^{n - 1} } {2^n} = \frac 1 2$
{{qed}}
Category:Probability
Category:Power Set
pv78lpi9zgqecjkaorejix3fvz1oc5a
Theorem: Expected Sum of Randomly Drawn Subset

Let $n$ be a positive integer.
Let $\sqbrk n = \set {1, 2, \ldots, n}$ be the set of integers between $1$ and $n$.
Equip $\powerset {\sqbrk n}$ with the discrete uniform distribution.
Let $\map \Sigma S$ be the sum of a subset $S \in \powerset {\sqbrk n}$.
Then:
:$\ds \expect {\map \Sigma S} = \frac {n \paren {n + 1} } 4$

Proof:
For each $k \in \sqbrk n$, define $1_k : \powerset {\sqbrk n} \to \set {0, 1}$ by:
:$\ds \map {1_k} A = \begin{cases}1 & k \in A \\ 0 & k \not \in A\end{cases}$
for each $A \in \powerset {\sqbrk n}$.
We can then write:
:$\ds \map \Sigma S = \sum_{k \mathop = 1}^n k \map {1_k} S$
From Expectation is Linear, we have:
:$\ds \expect {\map \Sigma S} = \sum_{k \mathop = 1}^n k \expect {1_k}$
From Integral of Characteristic Function, we have:
:$\expect {1_k} = \map \Pr {k \in S}$
From Probability that Uniformly Selected Subset contains Particular Element, we have:
:$\ds \map \Pr {k \in S} = \frac 1 2$
Hence, we have:
:$\ds \expect {\map \Sigma S} = \frac 1 2 \sum_{k \mathop = 1}^n k$ 
From Sum of Arithmetic Sequence, we have:
:$\ds \sum_{k \mathop = 1}^n k = \frac {n \paren {n + 1} } 2$
and hence:
:$\ds \expect {\map \Sigma S} = \frac {n \paren {n + 1} } 4$
{{qed}}
Category:Probability
Category:Power Set
jovcxg7oaps5g3pdd6pvol9ug63koxz
Theorem: Expected Number of Trials Until N Consecutive Successes

Let $0 < p \le 1$.
Let $N$ be a positive integer.
We conduct an experiment with probability of success $p$. 
We run this experiment until we see $N$ consecutive successes.
Then the expected number of trials until we see $N$ consecutive successes is:
:$\ds \sum_{k \mathop = 1}^N p^{-k} = \frac 1 p + \frac 1 {p^2} + \ldots + \frac 1 {p^N}$

Proof:
Let $E_N$ be the expected number of trials until we see $N$ consecutive successes.
We look to form a recurrence relation for $E_N$ with $N > 1$. 
First, we run the experiment until we see $N$ consecutive successes.
In expectation, this will take $E_{N - 1}$ trials.
There is a probability $p$ that our next trial will succeed.
In this case, we see $N$ consecutive successes after $1 + E_{N - 1}$ trial in expectation.
There is a probability $1 - p$ that our next trial will fail, meaning that we reset our tally and run the experiment from scratch. 
In this case, we have:
{{begin-itemize}}
{{item||an expected value of $E_{N - 1}$ for the first run of $N - 1$ consecutive successes}}
{{item||$1$ experiment that failed}}
{{item||an expected value of $E_N$ for the number of trials until the first run of $N$ successes (since we start from scratch).}}
{{end-itemize}}
This gives:
:$E_N = p \paren {1 + E_{N - 1} } + \paren {1 - p} \paren {1 + E_{N - 1} + E_N}$
Hence:
:$E_N = 1 + p E_{N - 1} + \paren {1 - p} E_{N - 1} + \paren {1 - p} E_N$
This can be simplified to:
:$E_N = 1 + E_{N - 1} + \paren {1 - p} E_N$
This can be rearranged to:
:$p E_N = 1 + E_{N - 1}$
so that:
:$E_N = p^{-1} + p^{-1} E_{N - 1}$
We now prove that:
:$\ds E_N = \sum_{k \mathop = 1}^N p^{-k}$
by mathematical induction.
Let $\map P N$ be the claim:
:$\ds E_N = \sum_{k \mathop = 1}^N p^{-k}$
Theorem: Probability that Three Dice are Rolled in Strictly Increasing Order

Roll three fair six-sided dice one by one, recording the upwards face each time.
The probability that the dice were rolled with upwards face  in strictly increasing order is $5/54$.

Proof:
Let $X_1, X_2, X_3$ be the values of the three rolls.
Let $E$ be the event that:
:$X_1 < X_2 < X_3$
Let $E'$ be the event that:
:$X_1$, $X_2$ and $X_3$ are all distinct. 
By Bayes' Theorem, we have:
:$\map \Pr E = \map \Pr {E \cap E'} = \map \Pr {E \mid E'} \map \Pr {E'}$
since $E' \subseteq E$.
Given that $X_1$, $X_2$ and $X_3$ are all distinct, there are $3! = 6$ permutations of their values by Number of Permutations of All Elements.
Hence there are $6$ possible orderings of the values of $X_1$, $X_2$ and $X_3$. 
Since the dice rolls are independent: 
:all orderings of $X_1$, $X_2$ and $X_3$ are equally likely
given that $X_1$, $X_2$ and $X_3$ are all distinct.
Hence:
:$\map \Pr {E \mid E'} = 1/6$
Using Bayes' Theorem, we have:
:$\map \Pr {E'} = \map \Pr {\paren {X_2 \ne X_1 \cap X_3 \ne X_1} \cap \paren {X_2 \ne X_1} } = \map \Pr {X_2 \ne X_1} \map \Pr {X_3 \ne X_2, \, X_3 \ne X_1 \mid X_2 \ne X_1}$
For a fixed value of $X_1$, the probability that $X_2$ does not take that value is $5/6$.
Hence:
:$\map \Pr {X_2 \ne X_1} = 5/6$ 
For fixed values of $X_1$ and $X_2$ such that $X_1 \ne X_2$, the probability that $X_3$ is not equal to either is $4/6$. 
Hence:
:$\ds \map \Pr {E'} = \frac {20} {36} = \frac 5 9$
To conclude:
:$\map \Pr E = \map \Pr {E \mid E'} \map \Pr {E'} = \dfrac 1 6 \times \dfrac 5 9 = \dfrac 5 {54}$
{{qed}}
Category:Probability
Category:Dice
9zcptyoajzujs5etma0xu073wijynwi
Theorem: Similar Matrices have Same Eigenvalues

Let $\mathbf A$ and $\mathbf B$ be similar matrices.
Then, every eigenvalue of $\mathbf A$ is an eigenvalue of $\mathbf B$ and vice versa.

Proof:
Follows directly from Similar Matrices have Same Characteristic Polynomial.
{{qed}}
Category:Matrix Similarity
Category:Eigenvalues of Square Matrices
ssyzamawrcyxcndurnqnrs02l2u8n3x
Theorem: Euler Phi Function of Power Minus One is Divisible by Exponent

Let $a, n \in \Z$ with $a \ge 2$ and $n \ge 1$.
Then:
:$n \divides \map \phi {a^n - 1}$
where $\phi$ is the Euler phi function.

Proof:
Clearly:
:$a^n = \paren {a^n - 1} + 1$
By definition of congruence:
:$a^n \equiv 1 \pmod {a^n - 1}$
From Power Function on Base Greater than One is Strictly Increasing:
:$\forall m \in \Z: 0 < m < n \implies 1 < a^m < a^n$
So $n$ is the multiplicative order of $a$ modulo $a^n - 1$.
The result follows from {{Corollary|Integer to Power of Multiple of Order}}.
{{qed}}
Category:Euler Phi Function
iou3kksoiuvianguq6ufdyexegjcgs6
Theorem: Determinant Equals Product of Eigenvalues

Let $\mathbf M$ be a square matrix over $\C$ of order $n$.
Let $\tuple {\lambda_1, \lambda_2, \ldots, \lambda_n}$ be the eigenvalues of $\mathbf M$ including algebraic multiplicity.
Then:
:$\ds \map \det {\mathbf M} = \prod_{i \mathop = 1}^n \lambda_i$

Proof:
The eigenvalues of $\mathbf M$ are the roots of its characteristic equation.
Thus:
{{begin-eqn}}
{{eqn | l = \map \det {\lambda \mathbf I - \mathbf M}
      | r = \prod_{i \mathop = 1}^n \paren {\lambda - \lambda_i}
      | c = Polynomial Factor Theorem
}}
{{eqn | ll= \leadsto
      | l = \map \det {-\mathbf M}
      | r = \prod_{i \mathop = 1}^n \paren {-\lambda_i}
      | c = Set $\lambda = 0$
}}
{{eqn | ll= \leadsto
      | l = \paren {-1}^n \map \det {\mathbf M}
      | r = \paren {-1}^n \prod_{i \mathop = 1}^n \lambda_i
      | c = Determinant of Matrix Multiplied by Constant
}}
{{eqn | ll= \leadsto
      | l = \map \det {\mathbf M}
      | r = \prod_{i \mathop = 1}^n \lambda_i
}}
{{end-eqn}}
{{qed}}
Theorem: Similar Matrices have Same Rank

Let $\mathbf A$ and $\mathbf B$ be similar square matrices of order $n$ over a field $\mathbb F$.
Then:
:$\map \rho {\mathbf A} = \map \rho {\mathbf B}$
where
:$\map \rho {\mathbf A}$ is the rank of $\mathbf A$

Proof:
=== Full Rank Case ===
Let $\mathbf A$ be full rank:
:$\map \rho {\mathbf A} = n$
Then, by Square Matrix has Full Rank iff Nonsingular, $\mathbf A$ is nonsingular.
Therefore:
:$\map \det {\mathbf A} \neq 0$
From Similar Matrices have Same Determinant:
:$\map \det {\mathbf A} = \map \det {\mathbf B}$
Thus:
:$\map \det {\mathbf B} \neq 0$
Thus, $\mathbf B$ is nonsingular.
Thus, $\mathbf B$ be full rank.
{{qed|lemma}}
Theorem: Determinant of Matrix Multiplied by Constant

Let $\mathbf M$ be a square matrix of order $n$ over a field $\mathbb F$.
Let $k$ be a scalar in $\mathbb F$.
Then:
:$\map \det {k \mathbf M} = k^n \map \det {\mathbf M}$

Proof:
For $1 \le i \le n$, let $e_i$ be the elementary row operation that multiplies row $i$ of $\mathbf A$ by $k$.
By definition of the scalar product, $k \mathbf A$ is obtained by multiplying every row of $\mathbf A$ by $k$.
That is the same as applying $e_i$ to $\mathbf A$ for each of $i \in \set {1, 2, \ldots, n}$.
Let $\mathbf E_i$ denote the elementary row matrix corresponding to $e_i$.
By Determinant of Elementary Row Matrix: Scale Row:
:$\map \det {\mathbf E_i} = k$
Then we have:
{{begin-eqn}}
{{eqn | l = k \mathbf A
      | r = \paren {\prod_{i \mathop = 1}^n \mathbf E_i} \mathbf A
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \det {k \mathbf A}
      | r = \map \det {\paren {\prod_{i \mathop = 1}^n \mathbf E_i} \mathbf A}
      | c = 
}}
{{eqn | r = \map \det {\prod_{i \mathop = 1}^n \mathbf E_i} \map \det {\mathbf A}
      | c = Determinant of Matrix Product
}}
{{eqn | r = \paren {\prod_{i \mathop = 1}^n \map \det {\mathbf E_i} } \map \det {\mathbf A}
      | c = Determinant of Matrix Product
}}
{{eqn | r = \paren {\prod_{i \mathop = 1}^n k} \map \det {\mathbf A}
      | c = Determinant of Elementary Row Matrix: Scale Row
}}
{{eqn | r = k^n \map \det {\mathbf A}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Rule of Transposition/Formulation 2/Forward Implication

:$\vdash \paren {p \implies q} \implies \paren {\neg q \implies \neg p}$

Proof:
{{BeginTableau |\vdash \paren {p \implies q} \implies \paren {\neg q \implies \neg p} }}
{{Assumption   |1|p \implies q}}
{{Assumption   |2|\neg q}}
{{ModusTollens |3|1, 2|\neg p|1|2}}
{{Implication  |4|1|\neg q \implies \neg p|2|3}}
{{Implication  |5||\paren {p \implies q} \implies \paren {\neg q \implies \neg p}|1|4}}
{{EndTableau|qed}}
Theorem: Rule of Transposition/Formulation 2/Forward Implication

:$\vdash \paren {p \implies q} \implies \paren {\neg q \implies \neg p}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth value under the main connective is true for all boolean interpretations.
:<nowiki>$\begin {array} {|ccc|c|ccccc|} \hline
(p & \implies & q) & \implies & (\neg & q & \implies & \neg & p) \\
\hline
\F & \T & \F & \T & \T & \F & \T & \T & \F \\
\F & \T & \T & \T & \F & \T & \T & \T & \F \\
\T & \F & \F & \T & \T & \F & \F & \F & \T \\
\T & \T & \T & \T & \F & \T & \T & \F & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Rule of Transposition/Formulation 2/Reverse Implication

:$\vdash \paren {\neg q \implies \neg p} \implies \paren {p \implies q}$

Proof:
{{BeginTableau|\vdash \paren {\neg q \implies \neg p} \implies \paren {p \implies q} }}
{{Assumption|1|\neg q \implies \neg p}}
{{Assumption|2|p}}
{{DoubleNegIntro|3|2|\neg \neg p|2}}
{{ModusTollens|4|1, 2|\neg \neg q|1|3}}
{{DoubleNegElimination|5|1, 2|q|4}}
{{Implication|6|1|p \implies q|2|5}}
{{Implication|7||\paren {\neg q \implies \neg p} \implies \paren {p \implies q}|1|6}}
{{EndTableau|qed}}
{{LEM|Double Negation Elimination|4}}
Theorem: Rule of Transposition/Formulation 2/Reverse Implication

:$\vdash \paren {\neg q \implies \neg p} \implies \paren {p \implies q}$

Proof:
We apply the Method of Truth Tables to the proposition.
As can be seen by inspection, the truth value under the main connective is is true for all boolean interpretations.
:<nowiki>$\begin {array} {|ccccc|c|ccc|} \hline
(\neg & q & \implies & \neg & p) & \implies & (p & \implies & q) \\
\hline
\T & \F & \T & \T & \F & \T & \F & \T & \F \\
\F & \T & \T & \T & \F & \T & \F & \T & \T \\
\T & \F & \F & \F & \T & \T & \T & \F & \F \\
\T & \T & \T & \F & \T & \T & \T & \T & \T \\
\hline
\end {array}$</nowiki>
{{qed}}
Theorem: Identity Mapping is Normal

The identity mapping is normal.

Proof:
Follows directly from Identity Mapping is Hermitian and Hermitian Operator is Normal.
Category:Identity Mappings
Category:Normal Operators
cy43ogpqgzu7rhz3l3qds6u6xh3z0f8