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

Update CrAnFieldOp.lean

Browse source
This commit is contained in:
jstoobysmith 2025-02-03 11:29:37 +00:00
parent 8f41de5785
commit 6433259bc4
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
View file

@ -86,15 +86,15 @@ def crAnFieldOpToCreateAnnihilate : 𝓕.CrAnFieldOp → CreateAnnihilate
def crAnStatistics : 𝓕.CrAnFieldOp → FieldStatistic :=
𝓕.statesStatistic ∘ 𝓕.crAnFieldOpToFieldOp
/-- The field statistic of a `CrAnState`. -/
/-- The field statistic of a `CrAnFieldOp`. -/
scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ =>
(crAnStatistics 𝓕) φ
/-- The field statistic of a list of `CrAnState`s. -/
/-- The field statistic of a list of `CrAnFieldOp`s. -/
scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
(crAnStatistics 𝓕) φ
/-- The `CreateAnnihilate` value of a `CrAnState`s, i.e. whether it is a creation or
/-- The `CreateAnnihilate` value of a `CrAnFieldOp`s, i.e. whether it is a creation or
annihilation operator. -/
scoped[FieldSpecification] infixl:80 "|>ᶜ" =>
crAnFieldOpToCreateAnnihilate