Documentation Verification Report

CreateAnnihilate

📁 Source: PhysLean/QFT/PerturbationTheory/CreateAnnihilate.lean

Statistics

Metric	Count
Definitions `CreateAnnihilate`, `instDecidableNormalOrder`, `instFintype`, `normalOrder`, `instBEqCreateAnnihilate`, `beq`, `instDecidableEqCreateAnnihilate`, `instInhabitedCreateAnnihilate`, `default`	9
Theorems `CreateAnnihilate_card_eq_two`, `eq_create_or_annihilate`, `instIsTotalNormalOrder`, `instIsTransNormalOrder`, `not_normalOrder_annihilate_iff_false`, `sum_eq`	6
Total	15

CreateAnnihilate

Definitions

Name	Category	Theorems
`instDecidableNormalOrder` 📖	CompOp	—
`instFintype` 📖	CompOp	2 math math: `sum_eq`, `CreateAnnihilate_card_eq_two`
`normalOrder` 📖	MathDef	3 math math: `not_normalOrder_annihilate_iff_false`, `instIsTotalNormalOrder`, `instIsTransNormalOrder`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`CreateAnnihilate_card_eq_two` 📖	mathematical	—	`CreateAnnihilate` `instFintype`	—	—
`eq_create_or_annihilate` 📖	mathematical	—	`create` `annihilate`	—	—
`instIsTotalNormalOrder` 📖	mathematical	—	`CreateAnnihilate` `normalOrder`	—	—
`instIsTransNormalOrder` 📖	mathematical	—	`CreateAnnihilate` `normalOrder`	—	—
`not_normalOrder_annihilate_iff_false` 📖	mathematical	—	`normalOrder` `annihilate`	—	—
`sum_eq` 📖	mathematical	—	`CreateAnnihilate` `instFintype` `create` `annihilate`	—	—

(root)

Definitions

Name	Category	Theorems
`CreateAnnihilate` 📖	CompData	4 math math: `CreateAnnihilate.sum_eq`, `CreateAnnihilate.instIsTotalNormalOrder`, `CreateAnnihilate.CreateAnnihilate_card_eq_two`, `CreateAnnihilate.instIsTransNormalOrder`
`instBEqCreateAnnihilate` 📖	CompOp	—
`instDecidableEqCreateAnnihilate` 📖	CompOp	—
`instInhabitedCreateAnnihilate` 📖	CompOp	—

instBEqCreateAnnihilate

Definitions

Name	Category	Theorems
`beq` 📖	CompOp	—

instInhabitedCreateAnnihilate

Definitions

Name	Category	Theorems
`default` 📖	CompOp	—

---

← Back to Index