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 2025-02-06 08:28:47 +00:00
parent 0eccb77459
commit 3f2593b5ff
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/PerturbationTheory/FieldSpecification/Basic.lean
View file

@ -36,8 +36,8 @@ These states carry the same field statistic as the field they are derived from.
- Real-scalar fields correspond to a single element of `positionDOF`.
- Complex-scalar fields correspond to two elements of `positionDOF`, one for the field and one
for its conjugate.
- Dirac fermions correspond to eight elements of `positionDOF`. One for each Lorentz index of the
field and its conjugate. (These are not all independent)
- Dirac fermions correspond to eight elements of `positionDOF`. One for each Lorentz index of
the field and its conjugate. (These are not all independent)
- Weyl fermions correspond to four elements of `positionDOF`. One for each Lorentz index of the
field. (These are not all independent)
- A type `asymptoticDOF` containing the degree-of-freedom in asymptotic field operators. Thus a