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

Update Proper.lean

Browse source
This commit is contained in:
jstoobysmith 2024-08-21 06:56:39 -04:00
parent 33f694169f
commit ede0e2d40c
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/Proper.lean
View file

@ -80,8 +80,8 @@ def detRep : 𝓛 d →* ℤ₂ where
map_mul' Λ1 Λ2 := by
simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero,
mul_ite, mul_one, ite_mul, one_mul]
cases' (det_eq_one_or_neg_one Λ1) with h1 h1
<;> cases' (det_eq_one_or_neg_one Λ2) with h2 h2
cases' det_eq_one_or_neg_one Λ1 with h1 h1
<;> cases' det_eq_one_or_neg_one Λ2 with h2 h2
<;> simp [h1, h2, detContinuous]
rfl