diff --git a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean index 731a40c..1dd8e43 100644 --- a/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean +++ b/HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean @@ -4,6 +4,15 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.StandardModel.HiggsBoson.Basic +/-! + +# The Two Higgs Doublet Model + +The two Higgs doublet model is the standard model plus an additional Higgs doublet. + +Currently this file contains the definition of the 2HDM optential. + +-/ namespace TwoHDM