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

Update Orthochronous.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-05-20 23:36:45 +02:00
parent 7088bfef3d
commit 503fd41712
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -112,7 +112,7 @@ lemma orthchroMapReal_minus_one_or_one (Λ : lorentzGroup) :
local notation "ℤ₂" => Multiplicative (ZMod 2)
/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
def orthchroMap : C(lorentzGroup, ℤ₂) :=
ContinuousMap.comp coeForℤ₂ {
toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
@ -169,7 +169,7 @@ lemma mul_not_othchron_of_not_othchron_othchron {Λ Λ' : lorentzGroup} (h : ¬
rw [zero_zero_mul]
exact euclid_norm_not_IsFourVelocity_IsFourVelocity h h'
/-- The representation from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
/-- The representation from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
def orthchroRep : lorentzGroup →* ℤ₂ where
toFun := orthchroMap
map_one' := by