refactor: lint

HepLean/Meta/Notes/ToHTML.lean

@@ -125,6 +125,8 @@ def codeButton : String := "
   }
 </style>
 "
+
+/-- HTML allowing the use of mathjax. -/
 def mathJaxScript : String := "
 <!-- MathJax code -->
 <script type=\"text/javascript\">

HepLean/PerturbationTheory/Wick/Algebra.lean

@@ -24,10 +24,8 @@ We will formally define the operator ring, in terms of the fields present in the
 - Tong, https://www.damtp.cam.ac.uk/user/tong/qft/qft.pdf
 -/
 
-
 namespace Wick
 
-
 note r"
 <h2>Operator algebra</h2>
 Given a Wick Species $S$, we can define the operator algebra of that theory.
@@ -98,7 +96,6 @@ informal_definition toWickAlgebra where
     returns the product of the fields in the monomial."
   deps :≈ [``WickAlgebra, ``WickMonomial]
 
-
 note r"
 <h2>Order</h2>
   "