PhysLean.QFT.PerturbationTheory.CreateAnnihilate

The type CreateAnnihilate is the type containing two elements create and annihilate. This type is used to specify if an operator is a creation, or annihilation, operator or the sum thereof or integral thereover etc.

create : CreateAnnihilate
annihilate : CreateAnnihilate

Instances For

source

instance instInhabitedCreateAnnihilate :

Inhabited CreateAnnihilate

Equations

instInhabitedCreateAnnihilate = { default := CreateAnnihilate.create }

source

instance instBEqCreateAnnihilate :

BEq CreateAnnihilate

Equations

instBEqCreateAnnihilate = { beq := beqCreateAnnihilate✝ }

source

instance instDecidableEqCreateAnnihilate :

DecidableEq CreateAnnihilate

Equations

instDecidableEqCreateAnnihilate x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

source

instance CreateAnnihilate.instFintype :

Fintype CreateAnnihilate

The type CreateAnnihilate is finite.

Equations

CreateAnnihilate.instFintype = { elems := {CreateAnnihilate.create , CreateAnnihilate.annihilate }, complete := CreateAnnihilate.instFintype.proof_1 }

source

theorem CreateAnnihilate.eq_create_or_annihilate (φ : CreateAnnihilate) :

φ = create ∨ φ = annihilate

source

def CreateAnnihilate.normalOrder :

CreateAnnihilate → CreateAnnihilate → Prop

The normal ordering on creation and annihilation operators. Under this relation, normalOrder a b is false only if a is annihilate and b is create.

Equations