docs(PauliMatrices): cite the published source for the three-Pauli identities

Physlib/Relativity/PauliMatrices/Relations.lean

@@ -18,6 +18,12 @@ for the Pauli four-vectors.
 The current way this result is proved is by using tensor tree manipulations.
 There is likely a more direct path to this result.
 
+## References
+
+* Dreiner, Haber and Martin, *Two-component spinor techniques and Feynman rules for quantum
+  field theory and supersymmetry*, arXiv:0812.1594, equations (2.54) and (2.55), in the
+  conventions `g = diag(+1, -1, -1, -1)` and `ε⁰¹²³ = +1`. [ref: Dreiner:2008tw]
+
 -/
 
 @[expose] public section
@@ -164,9 +170,9 @@ lemma leviCivita_mul_pauliDual :
   · decide
   · rfl
 
-/-- Equation (2.26), the three-Pauli identity
-`σ^μ barσ^ν σ^ρ = g^{μν} σ^ρ - g^{μρ} σ^ν + g^{νρ} σ^μ
-  + i ε^{μνρκ} σ_κ`, with barred and lowered forms expressed through index dualization `τ`. -/
+/-- The three-Pauli identity
+`σ^μ barσ^ν σ^ρ = g^{μν} σ^ρ - g^{μρ} σ^ν + g^{νρ} σ^μ + i ε^{μνρκ} σ_κ`,
+with barred and lowered forms expressed through index dualization `τ`. -/
 lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({
     σ^^^ | μ α β ⊗ σ^^^ | ν τ(α') τ(β) ⊗ σ^^^ | ρ α' β' =
       ((((η | μ ν ⊗ σ^^^ | ρ α β') + (-((η | μ ρ ⊗ σ^^^ | ν α β'))))
@@ -191,9 +197,9 @@ lemma pauliContr_mul_pauliContrDown_mul_pauliContr : ({
   apply Physlib.RatComplexNum.toComplexNum_eq_add_neg_add_add_iff.mpr
   decide +revert +kernel
 
-/-- Equation (2.27), the conjugate three-Pauli identity
-`barσ^μ σ^ν barσ^ρ = g^{μν} barσ^ρ - g^{μρ} barσ^ν + g^{νρ} barσ^μ
-  - i ε^{μνρκ} barσ_κ`, with barred and lowered forms expressed through index dualization `τ`. -/
+/-- The conjugate three-Pauli identity
+`barσ^μ σ^ν barσ^ρ = g^{μν} barσ^ρ - g^{μρ} barσ^ν + g^{νρ} barσ^μ - i ε^{μνρκ} barσ_κ`,
+with barred and lowered forms expressed through index dualization `τ`. -/
 lemma pauliContrDown_mul_pauliContr_mul_pauliContrDown : ({
     σ^^^ | μ τ(α) τ(β) ⊗ σ^^^ | ν α β' ⊗ σ^^^ | ρ τ(α') τ(β') =
       ((((η | μ ν ⊗ σ^^^ | ρ τ(α') τ(β))

docs/references.bib

@@ -33,8 +33,7 @@ @article{Dreiner:2008tw
   doi           = {10.1016/j.physrep.2010.05.002},
   journal       = {Phys. Rept.},
   pages         = {1-196},
-  year          = {2010},
-  note          = {not currently cited by any module; kept for future use}
+  year          = {2010}
 }
 
 @article{Lohitsiri:2019fuu,