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

refactor: Some lint

Browse source
This commit is contained in:
jstoobysmith 2024-07-11 09:20:27 -04:00
parent af1db2b6cb
commit 2681709f93
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/SpaceTime/LorentzTensor/Basic.lean
View file

@ -5,7 +5,6 @@ Authors: Joseph Tooby-Smith
-/
import HepLean.SpaceTime.LorentzVector.Basic
import Mathlib.CategoryTheory.Limits.FintypeCat
import LeanCopilot
/-!
# Lorentz Tensors
@ -158,6 +157,7 @@ lemma congrSet_refl : @congrSet d _ _ (Equiv.refl X) = Equiv.refl _ := by
## Rising and lowering indices
Rising or lowering an index corresponds to changing the color of that index.
-/
/-! TODO: Define the rising and lowering of indices using contraction with the metric. -/