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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-09-18 07:41:48 -04:00
parent 3aa00ff1e7
commit f1ad3433a4
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/SpaceTime/WeylFermion/Basic.lean
View file

@ -87,8 +87,8 @@ informal_lemma leftAltWeylFermionContraction_invariant where
deps :≈ [``leftAltWeylFermionContraction]
informal_definition altLeftWeylFermionContraction where
math :≈ "The linear map from altLeftHandedWeylFermion ⊗ leftHandedWeylFermion to ℂ given by
summing over components of altLeftHandedWeylFermion and leftHandedWeylFermion in the
math :≈ "The linear map from altLeftHandedWeylFermion ⊗ leftHandedWeylFermion to ℂ given by
summing over components of altLeftHandedWeylFermion and leftHandedWeylFermion in the
standard basis (i.e. the dot product)."
physics :≈ "The contraction of a left-handed Weyl fermion with a right-handed Weyl fermion.
In index notation this is φ^a ψ_a ."