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

refactor: add newline

Browse source
This commit is contained in:
jstoobysmith 2024-07-19 16:19:58 -04:00
parent bc79ff5920
commit b0f1ae79db
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
View file

@ -281,6 +281,7 @@ lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
## Sums ## Sums
-/ -/
/-- An equivalence that splits elements of `IndexValue d (Sum.elim TX TY)` into two components. -/ /-- An equivalence that splits elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} : def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where