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

feat: Informal def - One Particle Irreducible

Browse source
This commit is contained in:
jstoobysmith 2024-12-02 06:51:23 +00:00
parent 79cba76a2f
commit 75d6e3618c
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
HepLean/FeynmanDiagrams/Wick/Contract.lean
View file

@ -641,12 +641,16 @@ informal_definition HasEqualTimeContractions where
deps :≈ [``WickContract]
informal_definition IsConnected where
math :≈ "The condition for a Wick contraction that for any two vertices
math :≈ "The condition for a full Wick contraction that for any two vertices
(including external vertices) are connected by contractions."
deps :≈ [``WickContract]
informal_definition HasVacuumContributions where
math :≈ "The condition for a Wick contraction to have a vacuum contribution."
math :≈ "The condition for a full Wick contraction to have a vacuum contribution."
deps :≈ [``WickContract]
informal_definition IsOneParticleIrreducible where
math :≈ "The condition for a full Wick contraction to be one-particle irreducible."
deps :≈ [``WickContract]
end WickContract