WicksTheorem

Statistics

Metric	Count
Definitions	0
Theorems `wicks_theorem`, `wicks_theorem_congr`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`wicks_theorem` 📖	mathematical	—	`WickAlgebra` `FieldOpFreeAlgebra` `CrAnFieldOp` `fieldOpIdealSet` `WickAlgebra.timeOrder` `WickAlgebra.ofFieldOpList` `WickContraction` `FieldOp` `WickContraction.fintype_succ` `WickContraction.wickTerm`	—	`WickAlgebra.timeOrder_ofFieldOpList_nil` `WickContraction.sum_WickContraction_nil` `WickContraction.wickTerm_empty_nil` `eraseMaxTimeField_length` `WickAlgebra.timeOrder_eq_maxTimeField_mul_finset` `PhysLean.List.insertIdx_eraseIdx_fin` `wicks_theorem_congr` `WickContraction.insertLift_sum` `WickContraction.mul_wickTerm_eq_sum` `timeOrder_maxTimeField` `lt_maxTimeFieldPosFin_not_timeOrder` `FieldStatistic.exchangeSign_mul_self`
`wicks_theorem_congr` 📖	mathematical	—	`WickContraction` `FieldOp` `WickAlgebra` `FieldOpFreeAlgebra` `CrAnFieldOp` `fieldOpIdealSet` `WickContraction.fintype_succ` `WickContraction.wickTerm`	—	—

---