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

feat: space-time and self-adjoint matrices

Browse source
This commit is contained in:
jstoobysmith 2024-06-12 16:00:07 -04:00
parent 291ede435b
commit ea4327aff5
4 changed files with 101 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -6,6 +6,8 @@ Authors: Joseph Tooby-Smith
import HepLean.SpaceTime.Metric
import HepLean.SpaceTime.FourVelocity
import Mathlib.GroupTheory.SpecificGroups.KleinFour
import Mathlib.Geometry.Manifold.Algebra.LieGroup
import Mathlib.Analysis.Matrix
/-!
# The Lorentz Group