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 16:08:59 -04:00
parent eb21428c3e
commit fbda420da9
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/SpaceTime/AsSelfAdjointMatrix.lean
View file

@ -23,7 +23,7 @@ open Complex
/-- A 2×2-complex matrix formed from a space-time point. -/
@[simp]
def toMatrix (x : spaceTime) : Matrix (Fin 2) (Fin 2) ℂ :=
!![x 0 + x 3, x 1 - x 2 * I ; x 1 + x 2 * I, x 0 - x 3]
!![x 0 + x 3, x 1 - x 2 * I; x 1 + x 2 * I, x 0 - x 3]
/-- The matrix `x.toMatrix` for `x ∈ spaceTime` is self adjoint. -/
lemma toMatrix_isSelfAdjoint (x : spaceTime) : IsSelfAdjoint x.toMatrix := by