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

bump to v4.10.0-rc2

Browse source
This commit is contained in:
jstoobysmith 2024-07-26 16:32:54 -04:00
parent 689ce73a2b
commit b26f9e6691
7 changed files with 27 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -46,7 +46,6 @@ def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where
toFun x := if x = ⟨1, Set.mem_insert_of_mem (-1) rfl⟩
then (Additive.toMul 0) else (Additive.toMul (1 : ZMod 2))
continuous_toFun := by
haveI : DiscreteTopology ({-1, 1} : Set ℝ) := discrete_of_t1_of_finite
exact continuous_of_discreteTopology
/-- The continuous map taking a Lorentz matrix to its determinant. -/