Documentation Verification Report

SubContraction

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

Statistics

Metric	Count
Definitions `quotContraction`, `subContraction`	2
Theorems `mem_of_mem_quotContraction`, `mem_of_mem_subContraction`, `mem_quotContraction_iff`, `mem_subContraction_or_quotContraction`, `quotContraction_fstFieldOfContract_uncontractedListEmd`, `quotContraction_gradingCompliant`, `quotContraction_sndFieldOfContract_uncontractedListEmd`, `subContraction_fstFieldOfContract`, `subContraction_sndFieldOfContract`, `subContraction_uncontractedList_get`	10
Total	12

WickContraction

Definitions

Name	Category	Theorems
`quotContraction` 📖	CompOp	9 math math: `mem_quotContraction_iff`, `quotContraction_gradingCompliant`, `join_sub_quot`, `mem_subContraction_or_quotContraction`, `quotContraction_sndFieldOfContract_uncontractedListEmd`, `subContraction_card_plus_quotContraction_card_eq`, `quotContraction_eqTimeContractSet_not_haveEqTime`, `EqTimeOnly.quotContraction_eqTimeOnly`, `quotContraction_fstFieldOfContract_uncontractedListEmd`
`subContraction` 📖	CompOp	14 math math: `mem_quotContraction_iff`, `subContraction_sndFieldOfContract`, `quotContraction_gradingCompliant`, `join_sub_quot`, `mem_subContraction_or_quotContraction`, `quotContraction_sndFieldOfContract_uncontractedListEmd`, `subContraction_fstFieldOfContract`, `subContraction_card_plus_quotContraction_card_eq`, `quotContraction_eqTimeContractSet_not_haveEqTime`, `EqTimeOnly.quotContraction_eqTimeOnly`, `quotContraction_fstFieldOfContract_uncontractedListEmd`, `subContraction_eqTimeContractSet_eqTimeOnly`, `subContraction_singleton_eq_singleton`, `subContraction_uncontractedList_get`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_of_mem_quotContraction` 📖	mathematical	`FieldSpecification.FieldOp` `uncontractedListGet` `subContraction` `quotContraction`	`uncontractedListEmd`	—	—
`mem_of_mem_subContraction` 📖	—	`FieldSpecification.FieldOp` `subContraction`	—	—	—
`mem_quotContraction_iff` 📖	mathematical	`FieldSpecification.FieldOp`	`uncontractedListGet` `subContraction` `quotContraction` `uncontractedListEmd`	—	`mem_of_mem_quotContraction` `uncontractedListEmd_finset_not_mem` `mem_subContraction_or_quotContraction`
`mem_subContraction_or_quotContraction` 📖	mathematical	`FieldSpecification.FieldOp`	`subContraction` `uncontractedListGet` `uncontractedListEmd` `quotContraction`	—	`mem_uncontracted_iff_not_contracted` `uncontractedListEmd_surjective_mem_uncontracted`
`quotContraction_fstFieldOfContract_uncontractedListEmd` 📖	mathematical	`FieldSpecification.FieldOp`	`uncontractedListGet` `subContraction` `uncontractedListEmd` `fstFieldOfContract` `quotContraction` `mem_of_mem_quotContraction`	—	`mem_of_mem_quotContraction` `eq_fstFieldOfContract_of_mem` `uncontractedListEmd_strictMono` `fstFieldOfContract_lt_sndFieldOfContract`
`quotContraction_gradingCompliant` 📖	mathematical	`FieldSpecification.FieldOp` `GradingCompliant`	`uncontractedListGet` `subContraction` `quotContraction`	—	`subContraction_uncontractedList_get` `mem_of_mem_quotContraction` `quotContraction_fstFieldOfContract_uncontractedListEmd` `quotContraction_sndFieldOfContract_uncontractedListEmd`
`quotContraction_sndFieldOfContract_uncontractedListEmd` 📖	mathematical	`FieldSpecification.FieldOp`	`uncontractedListGet` `subContraction` `uncontractedListEmd` `sndFieldOfContract` `quotContraction` `mem_of_mem_quotContraction`	—	`mem_of_mem_quotContraction` `eq_sndFieldOfContract_of_mem` `uncontractedListEmd_strictMono` `fstFieldOfContract_lt_sndFieldOfContract`
`subContraction_fstFieldOfContract` 📖	mathematical	`FieldSpecification.FieldOp`	`fstFieldOfContract` `subContraction` `mem_of_mem_subContraction`	—	`eq_fstFieldOfContract_of_mem` `mem_of_mem_subContraction` `finset_eq_fstFieldOfContract_sndFieldOfContract` `fstFieldOfContract_lt_sndFieldOfContract`
`subContraction_sndFieldOfContract` 📖	mathematical	`FieldSpecification.FieldOp`	`sndFieldOfContract` `subContraction` `mem_of_mem_subContraction`	—	`eq_sndFieldOfContract_of_mem` `mem_of_mem_subContraction` `finset_eq_fstFieldOfContract_sndFieldOfContract` `fstFieldOfContract_lt_sndFieldOfContract`
`subContraction_uncontractedList_get` 📖	mathematical	`FieldSpecification.FieldOp`	`uncontractedListGet` `subContraction` `uncontractedListEmd`	—	`getElem_uncontractedListEmd`

---

← Back to Index