Fermionic algebra of the two-level annihilation $\sigma$ and creation $\ud{\sigma}$ operators, e.g., $[\ud{\sigma}\sigma,\ud{\sigma}^\mu\sigma^\nu]=(\mu-\nu)\ud{\sigma}^\mu\sigma^\nu$ as further detailed in our page on this subject and in my Electrodynamic's Wolverhampton Lectures on Physics, are extremely useful to speed up quantum algebra, provided that they are all correct and trustable. This page details the process of their verification.
First, this all follows from straightforward algebra:
$$\{\ud{\sigma},\sigma\}=\mathbb{1}$$
from which it is easy to get:
$$[\ud{\sigma},\sigma]=2\ud{\sigma}\sigma-\mathbb{1} \quad\text{and}\quad [\sigma,\ud{\sigma}]=\mathbb{1}-2\ud{\sigma}\sigma\,.$$
For our regmat method of computing such correlators, one has to find closure relations involving, typically, operators of the type $\ud{\sigma}^\mu\sigma^\nu$ where $\mu, \nu\in\{0,1\}$. They are easy enough to obtain in the first place, but easier still to make a mistake, somewhere. The last thing you want in a heavy calculation that you have checked several times is to eventually recognize that the mistake lies in one of the relations above. This is similar to the joke of the despaired womanizer who tells his friend that he received a note with the mention "if you still see my wife, I will kill you!" The friend asks what problem does that pause, since, with so many women acquaintances, he can just stop seeing this one? "The note was not signed!" weeps the other one. The following thus make sure that the mistake lies in your calculation, not in the identities above.
We are checking with Mathematica. A first thing to take care of is that this language does not take the 0th power of a singular matrix to be the identity, but takes it as undefined (like $0^0$), unlike, though, what is the custom practice (for matrices). See this discussion, from which we borrow the fix:
Unprotect[MatrixPower] MatrixPower[m_?SquareMatrixQ, 0] := IdentityMatrix[Length[m]] Protect[MatrixPower]
We define a commutator for brevity (as long as we will feed matrices, that is okay since their matrix product (the dot) is non-commutative):
Com[A_, B_] := A . B - B . A
The following identity:
$$[\ud{\sigma}\sigma,\ud{\sigma}^\mu\sigma^\nu]=(\mu-\nu)\ud{\sigma}^\mu\sigma^\nu$$
is thus checked by:
Table[Com[\[Sigma]d . \[Sigma], MatrixPower[\[Sigma]d, \[Mu]] . MatrixPower[\[Sigma], \[Nu]]] == (\[Mu] - \[Nu]) MatrixPower[\ \[Sigma]d, \[Mu]] . MatrixPower[\[Sigma], \[Nu]], {\[Mu], 0, 1}, {\[Nu], 0, 1}]
That returns:
{{True, True}, {True, True}}
To make sure, it is better to append a //Flatten//Union to get a simple:
{True}
Since we are checking a list, and that the code itself is not particularly readable, the code is written in a way that the identities are numbered and kept in the same order as the list above. So (note to self): if I add another identity, anywhere in the list, please make sure to retain the good order between this page, the footnotes of Electrodynamics and the Mathematica notebook, which is attached at the end of the page.