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

refactor: typo

Browse source
This commit is contained in:
jstoobysmith 2024-12-03 13:30:50 +00:00
parent ead93e7e8e
commit 723b2d1f82
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
HepLean/PerturbationTheory/FeynmanDiagrams/Light.lean
View file

@ -15,7 +15,7 @@ This file currently contains a lighter implmentation of Feynman digrams than can
The implmentation here is done in conjunction with Wicks species etc.
-/
/-! TODO Remove this namespace-/
/-! TODO: Remove this namespace-/
namespace LightFeynman
informal_definition FeynmanDiagram where
@ -55,7 +55,6 @@ informal_definition _root_.Wick.Contract.toFeynmanDiagram_isConnected_iff where
if and only if the Wick contraction is connected."
deps :≈ [``TwoComplexScalar.WickContract.IsConnected, ``FeynmanDiagram.IsConnected]
/-! TODO: Define an equivalence relation on Wick contracts related to the their underlying tensors
been equal after permutation. Show that two Wick contractions are equal under this
equivalence relation if and only if they have the same Feynman diagram. First step