Documentation Verification Report

Erase

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/Erase.lean

Statistics

Metric	Count
Definitions `erase`, `getDualErase`	2
Theorems `getDualErase_isSome_iff_getDual?_isSome`, `getDualErase_one`, `mem_erase_uncontracted_iff`, `mem_not_eq_erase_of_isNone`, `mem_not_eq_erase_of_isSome`	5
Total	7

WickContraction

Definitions

Name	Category	Theorems
`erase` 📖	CompOp	8 math math: `mem_not_eq_erase_of_isSome`, `insertAndContractNat_getDualErase`, `erase_insert`, `mem_erase_uncontracted_iff`, `mem_not_eq_erase_of_isNone`, `insertAndContractNat_erase`, `getDualErase_isSome_iff_getDual?_isSome`, `getDualErase_one`
`getDualErase` 📖	CompOp	4 math math: `insertAndContractNat_getDualErase`, `erase_insert`, `getDualErase_isSome_iff_getDual?_isSome`, `getDualErase_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`getDualErase_isSome_iff_getDual?_isSome` 📖	mathematical	—	`uncontracted` `erase` `getDualErase` `getDual?`	—	`getDual?_one_eq_none`
`getDualErase_one` 📖	mathematical	—	`getDualErase` `uncontracted` `erase`	—	—
`mem_erase_uncontracted_iff` 📖	mathematical	—	`uncontracted` `erase` `getDual?`	—	`getDual?_eq_some_iff_mem`
`mem_not_eq_erase_of_isNone` 📖	mathematical	`getDual?`	`erase`	—	`mem_uncontracted_iff_not_contracted`
`mem_not_eq_erase_of_isSome` 📖	mathematical	`getDual?`	`erase`	—	`getDual?_eq_some_iff_mem`

---

← Back to Index