FieldOpFreeAlgebra 📖 | CompOp | 333 mathmath: WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_mid, WickAlgebra.timeOrder_ofFieldOpList_nil, WickContraction.wickTerm_insert_some, WickAlgebra.fermionicProj_fermionicProj_eq_fermionicProj, WickAlgebra.timeContract_eq_smul, FieldOpFreeAlgebra.superCommuteF_expand_bosonicProjF_fermionicProjF, 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, WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder, FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul, 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, WickAlgebra.normalOrder_normalOrder_right, WickAlgebra.wicks_theorem_normal_order_empty, WickAlgebra.normalOrder_anPart_mul_anPart, FieldOpFreeAlgebra.ofCrAnListF_nil, WickContraction.join_sign_timeContract, FieldOpFreeAlgebra.normalOrderF_ofCrAnListF, WickAlgebra.bosonicProj_of_bosonic_part, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_mem_center, 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, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid, 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, 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, FieldOpFreeAlgebra.directSum_eq_bosonic_plus_fermionic, WickAlgebra.bosonicProj_add_fermionicProj, WickAlgebra.normalOrder_superCommute_left_eq_zero, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, 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, WickAlgebra.timeOrder_superCommute_eq_time_mid, WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_commute, WickAlgebra.anPart_superCommute_normalOrder_ofFieldOpList_sum, WickAlgebra.ofFieldOpList_append, WickAlgebra.anPart_eq_ι_anPartF, WickAlgebra.timeOrder_eq_maxTimeField_mul_finset, FieldOpFreeAlgebra.timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_eq_time, FieldOpFreeAlgebra.normalOrderF_mul_annihilate, 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, 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, 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, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF, WickAlgebra.timeOrder_timeOrder_right, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_ordered, FieldOpFreeAlgebra.normalOrderF_anPartF_mul_crPartF, WickAlgebra.wicks_theorem_normal_order, 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, WickAlgebra.anPart_mul_anPart_swap, WickContraction.join_timeContract, FieldOpFreeAlgebra.ofCrAnListF_mem_statisticSubmodule_of, 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, FieldOpFreeAlgebra.timeOrderF_timeOrderF_mid, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum, FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF, FieldOpFreeAlgebra.timeOrderF_ofFieldOpListF_nil, WickContraction.staticContract_of_not_gradingCompliant, FieldOpFreeAlgebra.anPartF_negAsymp, FieldOpFreeAlgebra.ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum, FieldOpFreeAlgebra.ofCrAnListF_append, WickContraction.wickTerm_empty_nil, WickContraction.timeContract_insert_some_of_lt, FieldOpFreeAlgebra.superCommuteF_anPartF_anPartF, WickAlgebra.superCommute_anPart_ofFieldOpList, WickAlgebra.timeOrder_timeContract_eq_time_mid, 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, 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, WickAlgebra.superCommute_ofCrAnList_ofCrAnList_symm, WickAlgebra.static_wick_theorem, WickContraction.timeContract_empty, WickAlgebra.ι_commute_fieldOpFreeAlgebra_superCommuteF_ofCrAnOpF_ofCrAnOpF, WickAlgebra.normalOrder_superCommute_right_eq_zero, FieldOpFreeAlgebra.normalOrderF_superCommuteF_crPartF_anPartF, FieldOpFreeAlgebra.timeOrderF_timeOrderF_left, WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, WickAlgebra.timeOrder_superCommute_neq_time, WickAlgebra.superCommute_crPart_anPart, WickAlgebra.ι_superCommuteF_of_annihilate_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, WickAlgebra.ofFieldOpList_cons, 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, WickAlgebra.universalLiftMap_ι, WickContraction.staticWickTerm_empty_nil, 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, FieldOpFreeAlgebra.ofFieldOpListF_nil, FieldOpFreeAlgebra.timeOrderF_ofCrAnListF, WickAlgebra.superCommute_create_create, FieldOpFreeAlgebra.ofFieldOpListF_sum, WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, WickAlgebra.crPart_mul_crPart_swap, WickAlgebra.ι_timeOrderF_superCommuteF_neq_time, FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpF, WickAlgebra.timeOrder_timeContract_neq_time, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul, WickAlgebra.ofFieldOp_eq_ι_ofFieldOpF, FieldOpFreeAlgebra.crPartF_posAsymp, FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF_if_bosonic, FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList, WickAlgebra.superCommuteRight_apply_ι, WickAlgebra.normalOrder_ofFieldOpList_anPart_swap, 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.universalLift_ι, WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute, FieldOpFreeAlgebra.normalOrderF_ofFieldOpF_mul_ofFieldOpF, FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF, WickAlgebra.anPart_inAsymp, WickAlgebra.bosonicProjFree_eq_ι_bosonicProjF, WickAlgebra.anPart_mul_crPart_eq_superCommute, WickAlgebra.fermionicProj_bosonicProj_eq_zero, 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, 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, FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_ordered, FieldOpFreeAlgebra.ofCrAnListF_bosonic_or_fermionic, WickContraction.EqTimeOnly.timeOrder_timeContract_of_not_eqTimeOnly, WickAlgebra.normalOrder_uncontracted_some, FieldOpFreeAlgebra.bosonicProjF_of_bonosic_part, FieldOpFreeAlgebra.anPartF_mul_crPartF_eq_superCommuteF, 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, WickAlgebra.superCommute_anPart_ofFieldOp_mem_center, FieldOpFreeAlgebra.ofListBasis_eq_ofList, FieldOpFreeAlgebra.timeOrderF_timeOrderF_right, WickAlgebra.ofCrAnOp_eq_ι_ofCrAnOpF, WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, 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, FieldOpFreeAlgebra.ofFieldOpF_eq_crPartF_add_anPartF, 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, WickAlgebra.ι_eq_zero_iff_mem_ideal, WickAlgebra.crPart_mul_normalOrder, WickAlgebra.ι_superCommuteF_of_create_create, FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_cons, WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, WickAlgebra.ofCrAnList_mem_statSubmodule_of_eq, WickAlgebra.universality, FieldOpFreeAlgebra.ofCrAnListF_cons, FieldOpFreeAlgebra.bosonicProjF_add_fermionicProjF, WickAlgebra.timeContract_inAsymp_inAsymp, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_commute, FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF, 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, WickAlgebra.normalOrder_one_eq_one, WickAlgebra.timeOrder_haveEqTime_split, FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpF, WickAlgebra.timeContract_of_not_timeOrderRel, 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, FieldOpFreeAlgebra.ofCrAnListF_injective
|