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

Update README.md

Browse source
This commit is contained in:
Joseph Tooby-Smith 2024-11-10 15:53:02 +00:00 • committed by GitHub
parent df210420ba
commit cd044a3b8e
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 11 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
README.md
View file

@ -19,7 +19,17 @@ into Lean 4.
3. Create good documentation so that the project can be used for pedagogical purposes.
## Areas of high energy physics with some coverage in HepLean
## Some parts of HepLean
__Lorentz [🗂️](https://heplean.github.io/HepLean/docs/HepLean/Lorentz/Group/Basic.html):__ The Lorentz group, Lorentz algebra, Weyl fermions, Real Lorentz vectors, complex Lorentz vectors, complex Lorentz tensors.
__Index notation [🗂️](https://heplean.github.io/HepLean/docs/HepLean/Tensors/OverColor/Basic.html):__ Formalization of index notation using category theory allowing commands like
```Lean
{A | μ ν ⊗ S | μ ν = - A | μ ν ⊗ S | μ ν}ᵀ
```
__Anomaly cancellation [🗂️](https://heplean.github.io/HepLean/docs/HepLean/AnomalyCancellation/Basic.html):__ Results related to solutions to the anomaly cancellation conditions of several theories.
[![](https://img.shields.io/badge/The_CKM_Matrix-blue)](https://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html)