Documentation Verification Report

Involutions

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

Statistics

Metric	Count
Definitions `equivInvolution`, `fromInvolution`, `toInvolution`	3
Theorems `fromInvolution_getDual?_eq_some`, `fromInvolution_getDual?_get`, `fromInvolution_getDual?_isSome`, `fromInvolution_toInvolution`, `toInvolution_fromInvolution`	5
Total	8

WickContraction

Definitions

Name	Category	Theorems
`equivInvolution` 📖	CompOp	—
`fromInvolution` 📖	CompOp	3 math math: `fromInvolution_toInvolution`, `fromInvolution_getDual?_isSome`, `toInvolution_fromInvolution`
`toInvolution` 📖	CompOp	2 math math: `fromInvolution_toInvolution`, `toInvolution_fromInvolution`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromInvolution_getDual?_eq_some` 📖	—	`getDual?` `fromInvolution`	—	—	`getDual?_eq_some_iff_mem`
`fromInvolution_getDual?_get` 📖	—	`getDual?` `fromInvolution`	—	—	`fromInvolution_getDual?_eq_some`
`fromInvolution_getDual?_isSome` 📖	mathematical	—	`getDual?` `fromInvolution`	—	`getDual?_isSome_iff`
`fromInvolution_toInvolution` 📖	mathematical	—	`toInvolution` `fromInvolution`	—	`fromInvolution_getDual?_get`
`toInvolution_fromInvolution` 📖	mathematical	—	`fromInvolution` `toInvolution`	—	`fstFieldOfContract_getDual?` `finset_eq_fstFieldOfContract_sndFieldOfContract`

---

← Back to Index