WickContractions

Statistics

Metric	Count
Definitions	0
Theorems `normalOrder_uncontracted_none`, `normalOrder_uncontracted_some`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`normalOrder_uncontracted_none` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `normalOrder` `ofFieldOpList` `WickContraction.uncontractedListGet` `FieldSpecification.FieldOp` `WickContraction.insertAndContract` `WickContraction.uncontracted` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset`	—	`ofFieldOpList_normalOrder_insert` `WickContraction.take_uncontractedListOrderPos_eq_filter` `WickContraction.uncontractedList_eq_sort` `FieldStatistic.exchangeSign_mul_self` `WickContraction.insertAndContract_uncontractedList_none_map`
`normalOrder_uncontracted_some` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `normalOrder` `ofFieldOpList` `WickContraction.uncontractedListGet` `FieldSpecification.FieldOp` `WickContraction.insertAndContract` `WickContraction.uncontracted` `PhysLean.List.optionEraseZ` `WickContraction.uncontractedFieldOpEquiv`	—	`WickContraction.congr_uncontractedList` `WickContraction.uncontractedList_extractEquiv_symm_some` `List.map_eraseIdx` `PhysLean.List.insertIdx_length_fin` `PhysLean.List.get_eq_insertIdx_succAbove`

---