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

Docs: Minor changes

Browse source
This commit is contained in:
jstoobysmith 2024-05-20 06:53:54 -04:00
parent 2f0377baf0
commit a40d21378b
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/SpaceTime/LorentzGroup/Boosts.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license.
Authors: Joseph Tooby-Smith Authors: Joseph Tooby-Smith
-/ -/
import HepLean.SpaceTime.LorentzGroup.Orthochronous import HepLean.SpaceTime.LorentzGroup.Orthochronous
import HepLean.SpaceTime.LorentzGroup.Proper
import Mathlib.GroupTheory.SpecificGroups.KleinFour import Mathlib.GroupTheory.SpecificGroups.KleinFour
import Mathlib.Topology.Constructions import Mathlib.Topology.Constructions
/-! /-!

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

@ -169,7 +169,7 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬
rw [zero_zero_mul] rw [zero_zero_mul]
exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h' exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h'
/-- The representation from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/ /-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
def orthchroRep : lorentzGroup →* ℤ₂ where def orthchroRep : lorentzGroup →* ℤ₂ where
toFun := orthchroMap toFun := orthchroMap
map_one' := by map_one' := by