diff --git a/HepLean.lean b/HepLean.lean index aa68e9e..ee22052 100644 --- a/HepLean.lean +++ b/HepLean.lean @@ -73,6 +73,7 @@ import HepLean.SpaceTime.LorentzGroup.Proper import HepLean.SpaceTime.LorentzGroup.Rotations import HepLean.SpaceTime.Metric import HepLean.SpaceTime.SL2C.Basic -import HepLean.StandardModel.HiggsBoson.TargetSpace +import HepLean.StandardModel.Basic import HepLean.StandardModel.HiggsBoson.Basic +import HepLean.StandardModel.HiggsBoson.TargetSpace import HepLean.StandardModel.Representations diff --git a/doc/index.markdown b/doc/index.markdown index d3837a5..19032ef 100644 --- a/doc/index.markdown +++ b/doc/index.markdown @@ -58,5 +58,5 @@ Any area not appearing in the below table has zero coverage in HepLean. | [Feynman diagrams](https://heplean.github.io/HepLean/docs/HepLean/FeynmanDiagrams/Basic.html) | ✔️ | ✘ | ✘ | | | [Lorentz Group](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) | ✔️ | ✘ | ✘ | New lemmas etc.| | [2HDM](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) | ✔️ | ✘ | ✘ | New lemmas etc. | - +| All other areas | ✘ | ✘ | ✘ | New lemmas etc.|