FieldOp 📖 | CompData | 213 mathmath: WickAlgebra.timeOrder_ofFieldOpList_nil, WickContraction.sign_insert_none_eq_signInsertNone_mul_sign, WickContraction.sign_empty, WickContraction.join_getDual?_apply_uncontractedListEmb_eq_none_iff, WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute, WickContraction.insertAndContract_uncontractedList_none_zero, WickAlgebra.timeOrder_ofFieldOpList_singleton, WickContraction.sign_insert_none_zero, CrAnSection.congr_trans_apply, WickContraction.signFinset_right_map_uncontractedListEmd_eq_filter, WickContraction.staticWickTerm_insert_zero_some, FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul, WickAlgebra.ofFieldOp_eq_sum, FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_singleton, FieldOpFreeAlgebra.ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF, wicks_theorem_congr, CrAnSection.take_congr, timeOrderList_eq_maxTimeField_timeOrderList, WickContraction.sign_right_eq_prod_mul_prod, WickContraction.join_fstFieldOfContract_joinLiftRight, CrAnSection.drop_left, WickAlgebra.wicks_theorem_normal_order_empty, timeOrderSign_nil, WickContraction.EqTimeOnly.eqTimeOnly_congr, crAnTimeOrderList_crAnSection_is_crAnSection, WickContraction.join_card, FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset, timeOrderSign_pair_ordered, WickAlgebra.normalOrder_ofFieldOpList_nil, WickContraction.jointLiftLeft_injective, FieldOpFreeAlgebra.ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, WickAlgebra.ofFieldOpList_normalOrder_insert, WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, maxTimeFieldPos_lt_length, WickContraction.insertAndContract_fstFieldOfContract, WickContraction.joinLift_injective, WickContraction.insertAndContract_some_getDual?_self_eq, WickContraction.gradingCompliant_congr, FieldOpFreeAlgebra.anPartF_posAsymp, WickContraction.insertAndContract_none_succAbove_getDual?_eq_none_iff, WickContraction.insertAndContract_some_getDual?_self_not_none, WickContraction.wickTerm_insert_none, FieldOpFreeAlgebra.ofFieldOpListF_append, crAnFieldOpToFieldOp_prod, WickContraction.stat_signFinset_right, WickContraction.mem_join_right_iff, CrAnSection.congr_snd_append, FieldOpFreeAlgebra.ofFieldOpListF_cons, WickContraction.insertAndContract_none_succAbove_getDual?_isSome_iff, crAnTimeOrderSign_crAnSection, WickContraction.uncontractedListEmd_finset_not_mem, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_cons, FieldOpFreeAlgebra.superCommuteF_ofFieldOpF_ofFieldOpFsList, WickContraction.self_not_mem_insertAndContractLiftFinset, WickContraction.joinLift_surjective, WickContraction.join_empty, WickContraction.signInsertNone_eq_filter_map, CrAnSection.congr_fst, WickAlgebra.anPart_superCommute_normalOrder_ofFieldOpList_sum, CrAnSection.sum_over_length, WickAlgebra.ofFieldOpList_append, WickContraction.timeContract_insert_none, WickAlgebra.timeOrder_eq_maxTimeField_mul_finset, WickContraction.getElem_uncontractedListEmd, CrAnSection.eq_head_cons_tail, WickContraction.uncontractedListEmd_toFun_eq_get, WickContraction.insertAndContract_sndFieldOfContract, instIsTotalFieldOpTimeOrderRel, WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList, WickContraction.insertAndContract_none_getDual?_self, WickContraction.join_assoc, CrAnSection.congr_symm, WickContraction.empty_not_haveEqTime, WickContraction.join_fstFieldOfContract_joinLiftLeft, FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpListF, WickContraction.insertAndContract_some_succAbove_getDual?_eq_option, WickAlgebra.ofFieldOpList_eq_sum, WickAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap, FieldOpFreeAlgebra.ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF, FieldOpFreeAlgebra.crPartF_negAsymp, WickAlgebra.wicks_theorem_normal_order, WickContraction.EqTimeOnly.exists_join_singleton_of_not_eqTimeOnly, maxTimeFieldPos_lt_eraseMaxTimeField_length_succ, FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF, WickContraction.insert_fin_eq_self, CrAnSection.append_assoc, FieldOpFreeAlgebra.ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, WickAlgebra.superCommute_ofFieldOp_ofFieldOpList, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum, FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_nil, CrAnSection.take_statistics_eq_take_state_statistics, WickContraction.uncontractedListEmd_empty, WickContraction.EqTimeOnly.eqTimeOnly_iff_forall_finset, WickContraction.join_eqTimeContractSet, WickContraction.join_uncontractedListEmb, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum, WickContraction.wickTerm_empty_nil, WickContraction.EqTimeOnly.empty_mem, WickAlgebra.superCommute_anPart_ofFieldOpList, WickContraction.insertAndContract_sndFieldOfContract_some_incl, WickContraction.staticContract_insert_some, WickContraction.uncontractedListGet_empty, WickContraction.insertAndContract_isSome_getDual?_self, WickContraction.mul_staticWickTerm_eq_sum, timeOrderList_nil, WickContraction.uncontractedFieldOpEquiv_list_sum, WickAlgebra.static_wick_theorem, WickContraction.join_getDual?_apply_uncontractedListEmb_isSome_iff, WickContraction.timeContract_empty, WickContraction.join_getDual?_apply_uncontractedListEmb, CrAnSection.statistics_eq_state_statistics, WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, WickContraction.stat_ofFinset_of_insertAndContractLiftFinset, WickContraction.succAbove_mem_insertAndContractLiftFinset, WickAlgebra.ofFieldOpList_singleton, FieldOpFreeAlgebra.crPartF_position, WickAlgebra.superCommute_crPart_ofFieldOpList, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpFsList, WickAlgebra.ofFieldOpList_cons, CrAnSection.singletonEquiv_append_eq_cons, WickContraction.staticWickTerm_empty_nil, WickContraction.insertAndContract_uncontractedList_none_map, WickAlgebra.normalOrder_uncontracted_none, WickAlgebra.superCommute_ofFieldOpList_ofFieldOp, WickContraction.signFinset_insertAndContract_some, CrAnSection.take_append_drop, FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpListF, FieldOpFreeAlgebra.ofFieldOpListF_nil, CrAnSection.length_eq, WickAlgebra.anPart_outAsymp, FieldOpFreeAlgebra.ofFieldOpListF_sum, WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, WickContraction.haveEqTime_iff_finset, WickContraction.join_sndFieldOfContract_joinLift, WickContraction.uncontractedListEmd_mem_uncontracted, CrAnSection.head_state_eq, CrAnSection.congr_append, timeOrderList_pair_not_ordered, FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList, WickAlgebra.normalOrder_ofFieldOpList_anPart_swap, FieldOpFreeAlgebra.anPartF_position, WickContraction.sign_congr, CrAnSection.card_eq_mul, WickContraction.signInsertNone_eq_prod_getDual?_Some, WickContraction.sum_haveEqTime, WickAlgebra.anPart_position, CrAnSection.card_cons_eq, WickContraction.stat_signFinset_insert_some_self_fst, FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpF, FieldOpFreeAlgebra.ofFieldOpListF_singleton, CrAnSection.sum_nil, WickContraction.insertLift_sum, timeOrderSign_pair_not_ordered, CrAnSection.append_assoc', WickContraction.staticContract_insert_none, WickContraction.insertAndContract_some_prod_contractions, CrAnSection.take_left, CrAnSection.drop_congr, WickContraction.eqTimeContractSet_subset, eraseMaxTimeField_length, WickContraction.jointLiftLeft_disjoint_joinLiftRight, WickContraction.Perm.perm_uncontractedList, FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF, WickAlgebra.crPart_position, WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute, timerOrderSign_of_eraseMaxTimeField, WickContraction.join_uncontractedList_get, timeOrderList_pair_ordered, WickAlgebra.normalOrder_uncontracted_some, WickContraction.sign_insert_some, WickContraction.insertAndContract_some_getDual?_some_eq, WickContraction.signInsertNone_eq_prod_prod, WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, WickContraction.timeContract_insertAndContract_some, WickAlgebra.ofFieldOpList_mul_ofFieldOpList_eq_superCommute, WickContraction.join_congr, WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, CrAnSection.card_nil_eq, WickAlgebra.normalOrder_anPart_ofFieldOpList_swap, instIsTransFieldOpTimeOrderRel, WickAlgebra.normalOrder_ofFieldOpList_mul_anPart_swap, WickContraction.signInsertNone_eq_filterset, WickAlgebra.superCommute_ofCrAnOp_ofFieldOpList_eq_sum, WickContraction.staticWickTerm_insert_zero_none, WickContraction.prod_join, WickContraction.stat_signFinset_insert_some_self_snd, WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute, WickContraction.insertAndContract_none_prod_contractions, WickContraction.insertAndContract_fstFieldOfContract_some_incl, WickContraction.eqTimeContractSet_of_mem_eqTimeOnly, WickContraction.joinLift_bijective, WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, CrAnSection.sum_cons, timeOrder_maxTimeField, CrAnSection.congr_fst_append, WickContraction.sign_insert_none, WickContraction.signFinset_insertAndContract_none, WickContraction.join_sndFieldOfContract_joinLiftRight, FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF, WickContraction.join_uncontractedList, FieldOpFreeAlgebra.anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, wicks_theorem, WickAlgebra.timeOrder_haveEqTime_split, WickContraction.joinLiftRight_injective, WickAlgebra.crPart_inAsymp, WickContraction.empty_join, WickContraction.signInsertNone_eq_mul_fst_snd, WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly, WickContraction.subContraction_singleton_eq_singleton, WickContraction.uncontractedFieldOpEquiv_none, WickContraction.eqTimeContractSet_of_not_haveEqTime, WickContraction.uncontractedListEmd_congr
|