From 291ede435b58b076ca0114e0d67ca06940297b42 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Wed, 12 Jun 2024 13:30:32 -0400
Subject: [PATCH] refactor: Lint

---
 HepLean/SpaceTime/LorentzAlgebra/Basis.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
index 2195dde..09bccb2 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
@@ -129,7 +129,7 @@ noncomputable def σCoordinateMap : lorentzAlgebra ≃ₗ[ℝ] Fin 6 →₀ ℝ
      cons_val_three, Fin.succ_one_eq_two, mul_neg, neg_zero, sub_zero, Finsupp.equivFunOnFinite]
 
 /-- The basis formed by the matrices `σ`. -/
-@[simps!]
+@[simps! repr_apply_support_val repr_apply_toFun]
 noncomputable def σBasis : Basis (Fin 6) ℝ lorentzAlgebra where
   repr := σCoordinateMap