CrAnFieldOp 📖 | CompOp | 408 mathmath: WickAlgebra.fermionicProjFree_eq_of_equiv, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_mid, instIsTransCrAnFieldOpNormTimeOrderRel, WickAlgebra.timeOrder_ofFieldOpList_nil, WickContraction.wickTerm_insert_some, WickAlgebra.fermionicProj_fermionicProj_eq_fermionicProj, normalOrderSign_cons_create, WickAlgebra.timeContract_eq_smul, FieldOpFreeAlgebra.superCommuteF_expand_bosonicProjF_fermionicProjF, crAnTimeOrderList_swap_eq_time, WickAlgebra.normalOrder_ofFieldOp_mul_ofFieldOp, WickContraction.staticContract_insert_some_of_lt, WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute, FieldOpFreeAlgebra.superCommuteF_anPartF_crPartF, WickAlgebra.normalOrder_ofCrAnList_nil, FieldOpFreeAlgebra.superCommuteF_crPartF_crPartF, WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero, FieldOpFreeAlgebra.normalOrderF_mul_anPartF, WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute, WickAlgebra.timeOrder_ofFieldOpList_singleton, WickAlgebra.fermionicProjFree_eq_ι_fermionicProjF, WickContraction.staticWickTerm_insert_zero_some, crAnTimeOrderList_pair_ordered, WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder, annihilateFilter_singleton_annihilate, FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul, normalOrderSign_swap_create_create_fst, WickAlgebra.crPart_outAsymp, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero, WickAlgebra.ofFieldOp_eq_sum, FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_singleton, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF, WickAlgebra.bosonicProj_fermionicProj_eq_zero, FieldOpFreeAlgebra.ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF, wicks_theorem_congr, WickAlgebra.crPart_eq_ι_crPartF, WickAlgebra.equiv_iff_exists_add, WickAlgebra.timeOrder_superCommute_eq_time_left, WickContraction.EqTimeOnly.timeOrder_staticContract_of_not_mem, FieldOpFreeAlgebra.fermionicProjF_mul, instIsTotalCrAnFieldOpNormalOrderRel, WickAlgebra.normalOrder_normalOrder_right, WickAlgebra.wicks_theorem_normal_order_empty, WickAlgebra.normalOrder_anPart_mul_anPart, FieldOpFreeAlgebra.ofCrAnListF_nil, WickContraction.join_sign_timeContract, normalOrderSign_singleton, FieldOpFreeAlgebra.normalOrderF_ofCrAnListF, WickAlgebra.bosonicProj_of_bosonic_part, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_mem_center, crAnTimeOrderList_crAnSection_is_crAnSection, WickAlgebra.timeOrder_superCommute_anPart_ofFieldOp_neq_time, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel, FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset, WickAlgebra.timeContract_outAsymp_outAsymp, WickAlgebra.normalOrder_ofFieldOpList_nil, FieldOpFreeAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, FieldOpFreeAlgebra.ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, WickAlgebra.ofFieldOpList_normalOrder_insert, FieldOpFreeAlgebra.ofCrAnOpF_bosonic_or_fermionic, WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, FieldOpFreeAlgebra.normalOrderF_swap_crPartF_anPartF, WickAlgebra.timeOrder_timeOrder_left, WickAlgebra.ι_normalOrderF_eq_of_equiv, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid, normalOrderSign_swap_create_annihilate_fst, FieldOpFreeAlgebra.normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF, WickAlgebra.timeContract_zero_of_diff_grade, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_left, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left, WickContraction.wickTerm_insert_none, FieldOpFreeAlgebra.ofFieldOpListF_append, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_symm, WickAlgebra.normalOrder_eq_ι_normalOrderF, WickAlgebra.superCommute_ofCrAnList_ofCrAnList, WickAlgebra.timeOrder_timeOrder, WickAlgebra.ofFieldOp_eq_crPart_add_anPart, WickAlgebra.superCommuteRight_apply_quot, FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered, FieldOpFreeAlgebra.ofFieldOpListF_cons, WickAlgebra.ι_of_mem_fieldOpIdealSet, FieldOpFreeAlgebra.superCommuteF_crPartF_anPartF, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction, FieldOpFreeAlgebra.mulLinearMap_apply, WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, FieldOpFreeAlgebra.normalOrderF_ofCrAnListF_cons_create, FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF, koszulSignInsert_create, FieldOpFreeAlgebra.directSum_eq_bosonic_plus_fermionic, WickAlgebra.bosonicProj_add_fermionicProj, WickAlgebra.normalOrder_superCommute_left_eq_zero, orderedInsert_annihilateFilter, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, crAnTimeOrderSign_crAnSection, WickAlgebra.timeOrder_timeContract_eq_time_left, WickAlgebra.mem_fermionic_iff_bosonicProj_eq_zero, WickAlgebra.ι_surjective, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_cons, FieldOpFreeAlgebra.superCommuteF_ofFieldOpF_ofFieldOpFsList, CrAnSection.congr_fst, WickAlgebra.timeOrder_superCommute_eq_time_mid, WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_commute, normalOrderList_eraseIdx_normalOrderEquiv, WickAlgebra.anPart_superCommute_normalOrder_ofFieldOpList_sum, CrAnSection.sum_over_length, WickAlgebra.ofFieldOpList_append, WickAlgebra.anPart_eq_ι_anPartF, WickAlgebra.timeOrder_eq_maxTimeField_mul_finset, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_eq_time, FieldOpFreeAlgebra.normalOrderF_mul_annihilate, CrAnSection.eq_head_cons_tail, FieldOpFreeAlgebra.normalOrderF_crPartF_mul_crPartF, WickAlgebra.ι_superCommuteF_of_diff_statistic, FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF, WickAlgebra.timeOrder_eq_ι_timeOrderF, WickAlgebra.timeContract_of_not_timeOrderRel_expand, WickAlgebra.ofCrAnList_eq_normalOrder, createFilter_cons_create, WickAlgebra.normalOrder_crPart_mul_crPart, WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList, FieldOpFreeAlgebra.normalOrderF_crPartF_mul_anPartF, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList, FieldOpFreeAlgebra.ofCrAnListF_eq_normalOrderF, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic, WickContraction.timeContract_insert_some_of_not_lt, WickAlgebra.normalOrder_crPart_mul_anPart, FieldOpFreeAlgebra.crPartF_mul_anPartF_eq_superCommuteF, WickAlgebra.ι_apply, normalOrderList_nil, FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpListF, WickAlgebra.ofCrAnOp_mul_ofCrAnList_eq_superCommute, WickAlgebra.ofFieldOpList_eq_sum, WickAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap, FieldOpFreeAlgebra.ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF, crAnTimeOrderList_pair_not_ordered, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF, FieldOpFreeAlgebra.ofCrAnListF_singleton, WickAlgebra.timeOrder_timeOrder_right, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_ordered, FieldOpFreeAlgebra.normalOrderF_anPartF_mul_crPartF, WickAlgebra.wicks_theorem_normal_order, normalOrderSign_append_annihilate, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right, FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_fermionic, FieldOpFreeAlgebra.normalOrderF_swap_anPartF_crPartF, FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul, FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF, koszulSignInsert_swap, WickAlgebra.anPart_mul_anPart_swap, WickContraction.join_timeContract, WickAlgebra.superCommute_anPart_ofFieldOp, FieldOpFreeAlgebra.ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldOpFreeAlgebra.normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF, WickAlgebra.superCommute_ofFieldOp_ofFieldOpList, WickAlgebra.bosonicProj_bosonicProj_eq_bosonicProj, FieldOpFreeAlgebra.bosonicProjF_of_fermionic_part, WickContraction.join_staticContract, normalOrderSign_swap_create_annihilate, FieldOpFreeAlgebra.timeOrderF_timeOrderF_mid, annihilateFilter_cons_annihilate, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum, createFilter_append, FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF, FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_nil, WickContraction.staticContract_of_not_gradingCompliant, CrAnSection.take_statistics_eq_take_state_statistics, FieldOpFreeAlgebra.anPartF_negAsymp, FieldOpFreeAlgebra.ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum, FieldOpFreeAlgebra.ofCrAnListF_append, WickContraction.wickTerm_empty_nil, orderedInsert_append_annihilate, WickContraction.timeContract_insert_some_of_lt, WickAlgebra.ofCrAnList_singleton, FieldOpFreeAlgebra.superCommuteF_anPartF_anPartF, WickAlgebra.superCommute_anPart_ofFieldOpList, WickAlgebra.timeOrder_timeContract_eq_time_mid, koszulSignInsert_crAnTimeOrderRel_crAnSection, WickContraction.staticContract_insert_some, WickAlgebra.fermionicProj_eq_fermionicProjFree, WickAlgebra.normalOrder_normalOrder_left, WickAlgebra.fermionicProj_of_fermionic_part, WickAlgebra.bosonicProj_eq_bosonicProjFree, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero, WickAlgebra.mem_bosonic_iff_fermionicProj_eq_zero, FieldOpFreeAlgebra.ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF, WickAlgebra.normalOrder_normalOrder, WickAlgebra.bosonicProj_of_fermionic_part, FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF, WickContraction.mul_staticWickTerm_eq_sum, createFilter_singleton_create, WickAlgebra.ofFieldOpList_eq_ι_ofFieldOpListF, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right, WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_mem_center, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel, WickAlgebra.ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero, crAnTimeOrderSign_swap_eq_time, WickAlgebra.superCommute_ofCrAnList_ofCrAnList_symm, WickAlgebra.static_wick_theorem, WickAlgebra.fermionicProjF_mem_fieldOpIdealSet_or_zero, WickContraction.timeContract_empty, WickAlgebra.ι_commute_fieldOpFreeAlgebra_superCommuteF_ofCrAnOpF_ofCrAnOpF, WickAlgebra.normalOrder_superCommute_right_eq_zero, FieldOpFreeAlgebra.normalOrderF_superCommuteF_crPartF_anPartF, FieldOpFreeAlgebra.timeOrderF_timeOrderF_left, CrAnSection.statistics_eq_state_statistics, sum_normalOrderList_length, WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, WickAlgebra.timeOrder_superCommute_neq_time, createFilter_singleton_annihilate, WickAlgebra.superCommute_crPart_anPart, WickAlgebra.ι_superCommuteF_of_annihilate_annihilate, orderedInsert_createFilter_append_annihilateFilter_annihilate, WickAlgebra.ι_timeOrderF_superCommuteF_eq_time, FieldOpFreeAlgebra.normalOrderF_superCommuteF_create_annihilate, FieldOpFreeAlgebra.normalOrderF_crPartF_mul, WickAlgebra.superCommute_crPart_ofFieldOpList, FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_symm, FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate, FieldOpFreeAlgebra.normalOrderF_normalOrderF_right, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpFsList, normalOrderSign_nil, WickAlgebra.ofFieldOpList_cons, normalOrderList_get_normalOrderEquiv, instIsTransCrAnFieldOpCrAnTimeOrderRel, crAnTimeOrderSign_pair_ordered, FieldOpFreeAlgebra.normalOrderF_anPartF_mul_anPartF, FieldOpFreeAlgebra.summerCommute_jacobi_ofCrAnListF, WickContraction.mul_wickTerm_eq_sum, WickAlgebra.timeContract_mem_center, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_left, FieldOpFreeAlgebra.anPartF_mul_anPartF_eq_superCommuteF, WickContraction.staticWickTerm_empty_nil, normalOrder_swap_create_annihilate_fst, WickAlgebra.fermionicProj_of_bosonic_part, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered, WickAlgebra.normalOrder_uncontracted_none, FieldOpFreeAlgebra.universality, WickAlgebra.superCommute_ofFieldOpList_ofFieldOp, WickAlgebra.normalOrder_anPart_mul_crPart, FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpListF, FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF, WickAlgebra.ofCrAnList_mem_statSubmodule, WickAlgebra.ι_normalOrder_superCommuteF_eq_zero_mul_right, WickAlgebra.normalOrder_superCommute_eq_zero, FieldOpFreeAlgebra.normalOrderF_one, orderedInsert_swap_eq_time, FieldOpFreeAlgebra.ofFieldOpListF_nil, CrAnSection.length_eq, FieldOpFreeAlgebra.timeOrderF_ofCrAnListF, WickAlgebra.superCommute_create_create, FieldOpFreeAlgebra.ofFieldOpListF_sum, koszulSignInsert_annihilate_cons_create, WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, WickAlgebra.crPart_mul_crPart_swap, WickAlgebra.ι_timeOrderF_superCommuteF_neq_time, normalOrderList_eq_createFilter_append_annihilateFilter, FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpF, instIsTransCrAnFieldOpNormalOrderRel, WickAlgebra.timeOrder_timeContract_neq_time, CrAnSection.head_state_eq, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul, WickAlgebra.ofFieldOp_eq_ι_ofFieldOpF, FieldOpFreeAlgebra.crPartF_posAsymp, annihilateFilter_cons_create, normalOrderSign_swap_create_create, normalOrderList_swap_create_annihilate, FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF_if_bosonic, FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList, WickAlgebra.superCommuteRight_apply_ι, WickAlgebra.normalOrder_ofFieldOpList_anPart_swap, CrAnSection.eraseIdxEquiv_symm_eraseIdx, WickAlgebra.ofFieldOp_mul_ofFieldOp_eq_superCommute, WickContraction.timeContract_of_not_gradingCompliant, FieldOpFreeAlgebra.normalOrderF_create_mul, FieldOpFreeAlgebra.crPartF_mul_crPartF_eq_superCommuteF, FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpF, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF, WickAlgebra.bosonicProjF_mem_fieldOpIdealSet_or_zero, CrAnSection.sum_nil, WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute, FieldOpFreeAlgebra.normalOrderF_ofFieldOpF_mul_ofFieldOpF, createFilter_cons_annihilate, FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF, WickAlgebra.anPart_inAsymp, WickAlgebra.bosonicProjFree_eq_ι_bosonicProjF, WickAlgebra.anPart_mul_crPart_eq_superCommute, WickAlgebra.fermionicProj_bosonicProj_eq_zero, instIsTotalCrAnFieldOpNormTimeOrderRel, FieldOpFreeAlgebra.fermionicProjF_of_bosonic_part, WickAlgebra.superCommute_anPart_crPart, FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_symm, WickAlgebra.superCommute_ofCrAnOp_ofCrAnList_eq_sum, crAnTimeOrderSign_nil, FieldOpFreeAlgebra.superCommuteF_superCommuteF_ofCrAnOpF_bosonic_or_fermionic, WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute, WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnListF, FieldOpFreeAlgebra.timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel, WickAlgebra.timeContract_of_timeOrderRel, instIsTotalCrAnFieldOpCrAnTimeOrderRel, FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_ordered, FieldOpFreeAlgebra.ofCrAnListF_bosonic_or_fermionic, WickContraction.EqTimeOnly.timeOrder_timeContract_of_not_eqTimeOnly, koszulSignInsert_append_annihilate, WickAlgebra.normalOrder_uncontracted_some, FieldOpFreeAlgebra.bosonicProjF_of_bonosic_part, FieldOpFreeAlgebra.anPartF_mul_crPartF_eq_superCommuteF, crAnTimeOrderSign_pair_not_ordered, orderedInsert_createFilter_append_annihilate, orderedInsert_crAnTimeOrderRel_crAnSection, annihilateFilter_append, WickAlgebra.equiv_iff_sub_mem_ideal, WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_fieldOpFreeAlgebra, WickAlgebra.superCommute_crPart_ofFieldOp, WickAlgebra.normalOrder_ofCrAnOp_ofCrAnList, FieldOpFreeAlgebra.normalOrderF_superCommuteF_anPartF_crPartF, WickAlgebra.normalOrder_ofCrAnList, WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, FieldOpFreeAlgebra.fermionicProjF_of_fermionic_part, WickAlgebra.ofCrAnList_append, WickAlgebra.superCommute_ofCrAnList_ofCrAnList_eq_sum, WickContraction.timeContract_insertAndContract_some, WickAlgebra.ofFieldOpList_mul_ofFieldOpList_eq_superCommute, crAnTimeOrderList_nil, WickAlgebra.superCommute_anPart_ofFieldOp_mem_center, FieldOpFreeAlgebra.ofListBasis_eq_ofList, FieldOpFreeAlgebra.timeOrderF_timeOrderF_right, WickAlgebra.ofCrAnOp_eq_ι_ofCrAnOpF, WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, WickAlgebra.bosonicProjFree_eq_of_equiv, FieldOpFreeAlgebra.bosonicProjF_mul, WickAlgebra.superCommute_crPart_crPart, WickAlgebra.normalOrder_timeContract, WickAlgebra.directSum_eq_bosonic_plus_fermionic, WickAlgebra.normalOrder_anPart_ofFieldOpList_swap, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero, WickAlgebra.normalOrder_mul_anPart, WickAlgebra.normalOrder_ofFieldOpList_mul_anPart_swap, WickAlgebra.ofCrAnList_eq_ι_ofCrAnListF, WickAlgebra.superCommute_anPart_ofFieldOpF_diff_grade_zero, WickAlgebra.superCommute_ofCrAnOp_ofFieldOpList_eq_sum, WickContraction.staticWickTerm_insert_zero_none, FieldOpFreeAlgebra.normalOrderF_normalOrderF_mid, normalOrderSign_swap_annihilate_annihilate_fst, FieldOpFreeAlgebra.ofFieldOpF_eq_crPartF_add_anPartF, normalOrderList_statistics, WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute, WickAlgebra.timeOrder_timeOrder_mid, WickAlgebra.normalOrder_ofFieldOp_ofFieldOp_swap, WickAlgebra.normalOrder_normalOrder_mid, FieldOpFreeAlgebra.normTimeOrder_ofCrAnListF, WickAlgebra.normalOrder_superCommute_mid_eq_zero, WickAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel', WickContraction.singleton_staticContract, WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero, FieldOpFreeAlgebra.normalOrderF_superCommuteF_annihilate_create, WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center, CrAnSection.eraseIdxEquiv_symm_getElem, WickAlgebra.ι_eq_zero_iff_mem_ideal, WickAlgebra.crPart_mul_normalOrder, WickAlgebra.ι_superCommuteF_of_create_create, orderedInsert_create, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_cons, WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, WickAlgebra.ι_timeOrderF_eq_of_equiv, FieldOpFreeAlgebra.ofCrAnListF_cons, normalOrderList_cons_create, FieldOpFreeAlgebra.bosonicProjF_add_fermionicProjF, WickAlgebra.timeContract_inAsymp_inAsymp, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_commute, annihilateFilter_singleton_create, FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF, normalOrderSign_eraseIdx, WickAlgebra.superCommute_annihilate_annihilate, FieldOpFreeAlgebra.bosonicProjF_ofCrAnListF, FieldOpFreeAlgebra.normalOrderF_ofCrAnListF_append_annihilate, WickAlgebra.crPart_mul_anPart_eq_superCommute, FieldOpFreeAlgebra.anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, WickContraction.singleton_timeContract, wicks_theorem, normalOrderSign_swap_annihilate_annihilate, WickAlgebra.normalOrder_one_eq_one, WickAlgebra.timeOrder_haveEqTime_split, FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpF, WickAlgebra.ι_superCommuteF_eq_of_equiv_right, WickAlgebra.timeContract_of_not_timeOrderRel, normalOrderList_append_annihilate, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_all_not_crAnTimeOrderRel, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul, WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnOpF, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul, WickAlgebra.timeOrder_ofFieldOpList_eqTimeOnly, WickAlgebra.superCommute_eq_ι_superCommuteF, WickAlgebra.superCommute_anPart_anPart, WickAlgebra.superCommute_diff_statistic, WickAlgebra.timeContract_eq_superCommute, FieldOpFreeAlgebra.normalOrderF_normalOrderF_left, WickAlgebra.ι_superCommuteF_ofCrAnOpF_superCommuteF_ofCrAnOpF_ofCrAnOpF, orderedInsert_in_swap_eq_time, FieldOpFreeAlgebra.ofCrAnListF_injective
|