DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-06-12 13:30:32 -04:00
parent 2bd3b64db7
commit 291ede435b
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/SpaceTime/LorentzAlgebra/Basis.lean
View file

@ -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