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

refactor: More TODO edits

Browse source
This commit is contained in:
jstoobysmith 2025-01-24 14:12:14 +00:00
parent 944fabca1a
commit 3740b5ba84
2 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/SpaceTime/Basic.lean
View file

@ -15,7 +15,7 @@ This file introduce 4d Minkowski spacetime.
noncomputable section
TODO "SpaceTime should be refactored into a structure, to prevent casting."
TODO "SpaceTime should be refactored into a structure, or similar, to prevent casting."
/-- The space-time -/
def SpaceTime : Type := Fin 4 → ℝ

1
HepLean/SpaceTime/CliffordAlgebra.lean
View file

@ -12,7 +12,6 @@ This file defines the Gamma matrices.
-/
TODO "Prove algebra generated by gamma matrices is isomorphic to Clifford algebra."
TODO "Define relations between the gamma matrices."
namespace spaceTime
open Complex