Basic

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/Sign/Basic.lean

Statistics

Metric	Count
Definitions sign, signFinset	2
Theorems sign_congr, sign_empty	2
Total	4

WickContraction

Definitions

Name	Category	Theorems
sign 📖	CompOp	26 math math: wickTerm_insert_some, sign_insert_none_eq_signInsertNone_mul_sign, sign_empty, sign_insert_none_zero, staticWickTerm_insert_zero_some, sign_right_eq_prod_mul_prod, join_singleton_sign_right, join_sign_timeContract, wickTerm_insert_none, sign_insert_some_of_not_lt, join_singleton_sign_left, sign_insert_some_zero, join_sign, FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, sign_congr, join_sign_induction, singleton_sign_expand, sign_insert_some, FieldSpecification.WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, staticWickTerm_insert_zero_none, sign_insert_some_of_lt, sign_insert_none, FieldSpecification.WickAlgebra.timeOrder_haveEqTime_split, FieldSpecification.WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly, join_sign_singleton
signFinset 📖	CompOp	14 math math: join_singleton_signFinset_eq_filter, signFinset_right_map_uncontractedListEmd_eq_filter, sign_right_eq_prod_mul_prod, join_singleton_sign_right, stat_signFinset_right, join_singleton_sign_left, signInsertSomeCoef_if, signFinset_insertAndContract_some, mem_signFinset, stat_signFinset_insert_some_self_fst, singleton_sign_expand, join_singleton_left_signFinset_eq_filter, stat_signFinset_insert_some_self_snd, signFinset_insertAndContract_none

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sign_congr 📖	mathematical	—	sign WickContraction FieldSpecification.FieldOp congr	—	—
sign_empty 📖	mathematical	—	sign empty FieldSpecification.FieldOp	—	sign.eq_1

---

← Back to Index