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

docs: Add comment about Lorentz vector

Browse source
This commit is contained in:
jstoobysmith 2024-11-08 05:30:07 +00:00
parent e2f06dd57f
commit c09780deb0
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/SpaceTime/LorentzVector/Basic.lean
View file

@ -24,7 +24,8 @@ corresponds to contravariant Lorentz tensors.
/- The number of space dimensions . -/
variable (d : ℕ)
/-- The type of (contravariant) Lorentz Vectors in `d`-space dimensions. -/
/-- The type of Lorentz Vectors in `d`-space dimensions.
This is very weak definition of a Lorentz vector. -/
def LorentzVector : Type := (Fin 1 ⊕ Fin d) → ℝ
/-- An instance of an additive commutative monoid on `LorentzVector`. -/