From e11bf41f4cbc24be09c407970c6a4d080a24cb6a Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 25 Oct 2024 13:52:06 +0000
Subject: [PATCH] refactor: Change bispinor name

---
 HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
index 950f01f..3ffef43 100644
--- a/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
+++ b/HepLean/Tensors/ComplexLorentz/Bispinors/Basic.lean
@@ -30,9 +30,9 @@ def contrBispinorUp (p : complexContr) :=
   {p | μ ⊗ pauliCo | μ α β}ᵀ.tensor
 
 /-- A bispinor `pₐₐ` created from a lorentz vector  `p^μ`. -/
-def bispinorDown (p : complexContr) :=
+def contrBispinorDown (p : complexContr) :=
   {Fermion.altRightMetric | β β' ⊗ Fermion.altLeftMetric | α α' ⊗
-    (complexContr.bispinorUp p) | α β}ᵀ.tensor
+    (contrBispinorUp p) | α β}ᵀ.tensor
 
 end complexLorentzTensor
 end