Documentation Verification Report

Singleton

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

Statistics

Metric	Count
Definitions `singleton`	1
Theorems `mem_signFinset`, `mem_singleton`, `mem_singleton_iff`, `of_singleton_eq`, `singleton_fstFieldOfContract`, `singleton_getDual?_eq_none_iff_neq`, `singleton_prod`, `singleton_sign_expand`, `singleton_sndFieldOfContract`, `singleton_staticContract`, `singleton_timeContract`, `singleton_uncontractedEmd_neq_left`, `singleton_uncontractedEmd_neq_right`, `subContraction_singleton_eq_singleton`	14
Total	15

WickContraction

Definitions

Name	Category	Theorems
`singleton` 📖	CompOp	23 math math: `join_singleton_signFinset_eq_filter`, `EqTimeOnly.exists_join_singleton_of_card_ge_zero`, `singleton_prod`, `join_singleton_sign_right`, `mem_singleton_iff`, `singleton_getDual?_eq_none_iff_neq`, `EqTimeOnly.exists_join_singleton_of_not_eqTimeOnly`, `join_singleton_sign_left`, `singleton_sndFieldOfContract`, `joinSignRightExtra_eq_i_j_finset_eq_if`, `of_singleton_eq`, `singleton_fstFieldOfContract`, `join_singleton_getDual?_left`, `mem_signFinset`, `exists_join_singleton_of_card_ge_zero`, `join_singleton_getDual?_right`, `singleton_sign_expand`, `join_singleton_left_signFinset_eq_filter`, `singleton_staticContract`, `singleton_timeContract`, `mem_singleton`, `join_sign_singleton`, `subContraction_singleton_eq_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_signFinset` 📖	mathematical	—	`signFinset` `singleton`	—	`singleton_getDual?_eq_none_iff_neq`
`mem_singleton` 📖	mathematical	—	`singleton`	—	—
`mem_singleton_iff` 📖	mathematical	—	`singleton`	—	—
`of_singleton_eq` 📖	mathematical	—	`singleton` `mem_singleton`	—	`mem_singleton_iff`
`singleton_fstFieldOfContract` 📖	mathematical	—	`fstFieldOfContract` `singleton` `mem_singleton`	—	`eq_fstFieldOfContract_of_mem` `mem_singleton`
`singleton_getDual?_eq_none_iff_neq` 📖	mathematical	—	`getDual?` `singleton`	—	`getDual?_eq_none_iff_mem_uncontracted` `mem_uncontracted_iff_not_contracted`
`singleton_prod` 📖	mathematical	`FieldSpecification.FieldOp`	`singleton` `mem_singleton`	—	`mem_singleton` `of_singleton_eq`
`singleton_sign_expand` 📖	mathematical	`FieldSpecification.FieldOp`	`sign` `singleton` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `signFinset`	—	`sign.eq_1` `mem_singleton` `singleton_prod` `singleton_sndFieldOfContract` `singleton_fstFieldOfContract`
`singleton_sndFieldOfContract` 📖	mathematical	—	`sndFieldOfContract` `singleton` `mem_singleton`	—	`eq_sndFieldOfContract_of_mem` `mem_singleton`
`singleton_staticContract` 📖	mathematical	`FieldSpecification.FieldOp`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `staticContract` `singleton` `FieldSpecification.WickAlgebra.superCommute` `FieldSpecification.WickAlgebra.anPart` `FieldSpecification.WickAlgebra.ofFieldOp`	—	`staticContract.eq_1` `mem_singleton` `singleton_prod` `singleton_fstFieldOfContract` `singleton_sndFieldOfContract`
`singleton_timeContract` 📖	mathematical	`FieldSpecification.FieldOp`	`timeContract` `singleton` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `FieldSpecification.WickAlgebra.timeContract` `FieldSpecification.WickAlgebra.timeContract_mem_center`	—	`FieldSpecification.WickAlgebra.timeContract_mem_center` `timeContract.eq_1` `mem_singleton` `singleton_prod` `singleton_fstFieldOfContract` `singleton_sndFieldOfContract`
`singleton_uncontractedEmd_neq_left` 📖	—	`FieldSpecification.FieldOp`	—	—	`mem_uncontracted_iff_not_contracted`
`singleton_uncontractedEmd_neq_right` 📖	—	`FieldSpecification.FieldOp`	—	—	`mem_uncontracted_iff_not_contracted`
`subContraction_singleton_eq_singleton` 📖	mathematical	—	`subContraction` `FieldSpecification.FieldOp` `singleton` `fstFieldOfContract` `sndFieldOfContract` `fstFieldOfContract_lt_sndFieldOfContract`	—	`fstFieldOfContract_lt_sndFieldOfContract` `finset_eq_fstFieldOfContract_sndFieldOfContract`

---

← Back to Index