| Name | Category | Theorems |
|---|
WickAlgebra 📖 | CompOp | 225 mathmath: WickAlgebra.fermionicProjFree_eq_of_equiv, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder, WickAlgebra.timeOrder_ofFieldOpList_nil, WickContraction.wickTerm_insert_some, WickAlgebra.fermionicProj_fermionicProj_eq_fermionicProj, WickAlgebra.timeContract_eq_smul, WickAlgebra.normalOrder_ofFieldOp_mul_ofFieldOp, WickContraction.staticContract_insert_some_of_lt, WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute, WickAlgebra.normalOrder_ofCrAnList_nil, WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero, 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, WickAlgebra.crPart_outAsymp, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero, WickAlgebra.ofFieldOp_eq_sum, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF, WickAlgebra.bosonicProj_fermionicProj_eq_zero, wicks_theorem_congr, WickAlgebra.crPart_eq_ι_crPartF, WickAlgebra.timeOrder_superCommute_eq_time_left, WickContraction.EqTimeOnly.timeOrder_staticContract_of_not_mem, WickAlgebra.normalOrder_normalOrder_right, WickAlgebra.wicks_theorem_normal_order_empty, WickAlgebra.normalOrder_anPart_mul_anPart, WickContraction.join_sign_timeContract, WickAlgebra.bosonicProj_of_bosonic_part, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_mem_center, WickAlgebra.timeOrder_superCommute_anPart_ofFieldOp_neq_time, WickAlgebra.timeContract_outAsymp_outAsymp, WickAlgebra.normalOrder_ofFieldOpList_nil, WickAlgebra.ofFieldOpList_normalOrder_insert, WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, WickAlgebra.timeOrder_timeOrder_left, WickAlgebra.ι_normalOrderF_eq_of_equiv, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid, WickAlgebra.timeContract_zero_of_diff_grade, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_left, WickContraction.wickTerm_insert_none, 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, WickAlgebra.ι_of_mem_fieldOpIdealSet, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction, WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, WickAlgebra.bosonicProj_add_fermionicProj, WickAlgebra.normalOrder_superCommute_left_eq_zero, WickAlgebra.timeOrder_timeContract_eq_time_left, WickAlgebra.mem_fermionic_iff_bosonicProj_eq_zero, WickAlgebra.ι_surjective, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul, 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, WickAlgebra.ι_superCommuteF_of_diff_statistic, WickAlgebra.timeOrder_eq_ι_timeOrderF, WickAlgebra.timeContract_of_not_timeOrderRel_expand, WickAlgebra.ofCrAnList_eq_normalOrder, WickAlgebra.normalOrder_crPart_mul_crPart, WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList, WickContraction.timeContract_insert_some_of_not_lt, WickAlgebra.normalOrder_crPart_mul_anPart, WickAlgebra.ι_apply, WickAlgebra.mem_fermionic_of_mem_free_fermionic, WickAlgebra.ofCrAnOp_mul_ofCrAnList_eq_superCommute, WickAlgebra.ofFieldOpList_eq_sum, WickAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF, WickAlgebra.mem_bosonic_of_mem_free_bosonic, WickAlgebra.timeOrder_timeOrder_right, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_ordered, WickAlgebra.wicks_theorem_normal_order, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul, WickAlgebra.anPart_mul_anPart_swap, WickContraction.join_timeContract, WickAlgebra.superCommute_anPart_ofFieldOp, WickAlgebra.superCommute_ofFieldOp_ofFieldOpList, WickAlgebra.bosonicProj_bosonicProj_eq_bosonicProj, WickContraction.join_staticContract, WickContraction.staticContract_of_not_gradingCompliant, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum, WickContraction.wickTerm_empty_nil, WickContraction.timeContract_insert_some_of_lt, 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, WickAlgebra.normalOrder_normalOrder, WickAlgebra.bosonicProj_of_fermionic_part, WickContraction.mul_staticWickTerm_eq_sum, WickAlgebra.ofFieldOpList_eq_ι_ofFieldOpListF, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right, WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_mem_center, WickAlgebra.ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero, WickAlgebra.ι_normalOrderF_zero_of_mem_ideal, WickAlgebra.superCommute_ofCrAnList_ofCrAnList_symm, WickAlgebra.static_wick_theorem, WickContraction.timeContract_empty, WickAlgebra.ι_commute_fieldOpFreeAlgebra_superCommuteF_ofCrAnOpF_ofCrAnOpF, WickAlgebra.normalOrder_superCommute_right_eq_zero, 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, WickAlgebra.superCommute_crPart_ofFieldOpList, WickAlgebra.ofFieldOpList_cons, WickContraction.mul_wickTerm_eq_sum, WickAlgebra.timeContract_mem_center, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_left, WickAlgebra.universalLiftMap_ι, WickContraction.staticWickTerm_empty_nil, WickAlgebra.fermionicProj_of_bosonic_part, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered, WickAlgebra.normalOrder_uncontracted_none, WickAlgebra.superCommute_ofFieldOpList_ofFieldOp, WickAlgebra.normalOrder_anPart_mul_crPart, WickAlgebra.ofCrAnList_mem_statSubmodule, WickAlgebra.ι_normalOrder_superCommuteF_eq_zero_mul_right, WickAlgebra.normalOrder_superCommute_eq_zero, WickAlgebra.superCommute_create_create, WickAlgebra.ι_superCommuteF_zero_of_fermionic, WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, WickAlgebra.crPart_mul_crPart_swap, WickAlgebra.ι_timeOrderF_superCommuteF_neq_time, WickAlgebra.timeOrder_timeContract_neq_time, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul, WickAlgebra.ofFieldOp_eq_ι_ofFieldOpF, WickAlgebra.superCommuteRight_apply_ι, WickAlgebra.mem_statSubmodule_of_mem_statisticSubmodule, WickAlgebra.normalOrder_ofFieldOpList_anPart_swap, WickAlgebra.ofFieldOp_mul_ofFieldOp_eq_superCommute, WickContraction.timeContract_of_not_gradingCompliant, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF, WickAlgebra.ι_superCommuteF_right_zero_of_mem_ideal, WickAlgebra.universalLift_ι, WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute, WickAlgebra.anPart_inAsymp, WickAlgebra.bosonicProjFree_eq_ι_bosonicProjF, WickAlgebra.anPart_mul_crPart_eq_superCommute, WickAlgebra.fermionicProj_bosonicProj_eq_zero, WickAlgebra.superCommute_anPart_crPart, WickAlgebra.superCommute_ofCrAnOp_ofCrAnList_eq_sum, WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute, WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnListF, WickAlgebra.timeContract_of_timeOrderRel, WickContraction.EqTimeOnly.timeOrder_timeContract_of_not_eqTimeOnly, WickAlgebra.normalOrder_uncontracted_some, WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_fieldOpFreeAlgebra, WickAlgebra.superCommute_crPart_ofFieldOp, WickAlgebra.normalOrder_ofCrAnOp_ofCrAnList, WickAlgebra.normalOrder_ofCrAnList, WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, 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, WickAlgebra.ofCrAnOp_eq_ι_ofCrAnOpF, WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, WickAlgebra.bosonicProjFree_eq_of_equiv, 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, WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute, WickAlgebra.timeOrder_timeOrder_mid, WickAlgebra.normalOrder_ofFieldOp_ofFieldOp_swap, WickAlgebra.normalOrder_normalOrder_mid, WickAlgebra.normalOrder_superCommute_mid_eq_zero, WickAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, WickContraction.singleton_staticContract, WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero, WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center, WickAlgebra.ι_eq_zero_iff_mem_ideal, WickAlgebra.crPart_mul_normalOrder, WickAlgebra.ι_superCommuteF_of_create_create, WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, WickAlgebra.ofCrAnList_mem_statSubmodule_of_eq, WickAlgebra.universality, WickAlgebra.ι_timeOrderF_eq_of_equiv, WickAlgebra.timeContract_inAsymp_inAsymp, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_commute, WickAlgebra.ι_timeOrderF_zero_of_mem_ideal, WickAlgebra.superCommute_annihilate_annihilate, WickAlgebra.crPart_mul_anPart_eq_superCommute, WickContraction.singleton_timeContract, wicks_theorem, WickAlgebra.normalOrder_one_eq_one, WickAlgebra.timeOrder_haveEqTime_split, WickAlgebra.ι_superCommuteF_eq_of_equiv_right, WickAlgebra.timeContract_of_not_timeOrderRel, 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, WickAlgebra.ι_superCommuteF_ofCrAnOpF_superCommuteF_ofCrAnOpF_ofCrAnOpF
|
fieldOpIdealSet 📖 | CompOp | 223 mathmath: WickAlgebra.fermionicProjFree_eq_of_equiv, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder, WickAlgebra.timeOrder_ofFieldOpList_nil, WickContraction.wickTerm_insert_some, WickAlgebra.fermionicProj_fermionicProj_eq_fermionicProj, WickAlgebra.timeContract_eq_smul, WickAlgebra.normalOrder_ofFieldOp_mul_ofFieldOp, WickContraction.staticContract_insert_some_of_lt, WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute, WickAlgebra.normalOrder_ofCrAnList_nil, WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero, 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, WickAlgebra.crPart_outAsymp, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero, WickAlgebra.ofFieldOp_eq_sum, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF, WickAlgebra.bosonicProj_fermionicProj_eq_zero, 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, WickAlgebra.normalOrder_normalOrder_right, WickAlgebra.wicks_theorem_normal_order_empty, WickAlgebra.normalOrder_anPart_mul_anPart, WickContraction.join_sign_timeContract, WickAlgebra.bosonicProj_of_bosonic_part, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_mem_center, WickAlgebra.timeOrder_superCommute_anPart_ofFieldOp_neq_time, WickAlgebra.timeContract_outAsymp_outAsymp, WickAlgebra.normalOrder_ofFieldOpList_nil, WickAlgebra.ofFieldOpList_normalOrder_insert, WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, WickAlgebra.timeOrder_timeOrder_left, WickAlgebra.ι_normalOrderF_eq_of_equiv, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid, WickAlgebra.timeContract_zero_of_diff_grade, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_left, WickContraction.wickTerm_insert_none, 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, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction, WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, WickAlgebra.bosonicProj_add_fermionicProj, WickAlgebra.normalOrder_superCommute_left_eq_zero, WickAlgebra.timeOrder_timeContract_eq_time_left, WickAlgebra.mem_fermionic_iff_bosonicProj_eq_zero, WickAlgebra.ι_surjective, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul, 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, WickAlgebra.ι_superCommuteF_of_diff_statistic, WickAlgebra.timeOrder_eq_ι_timeOrderF, WickAlgebra.timeContract_of_not_timeOrderRel_expand, WickAlgebra.ofCrAnList_eq_normalOrder, WickAlgebra.normalOrder_crPart_mul_crPart, WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList, WickContraction.timeContract_insert_some_of_not_lt, WickAlgebra.normalOrder_crPart_mul_anPart, WickAlgebra.ι_apply, WickAlgebra.mem_fermionic_of_mem_free_fermionic, WickAlgebra.ofCrAnOp_mul_ofCrAnList_eq_superCommute, WickAlgebra.ofFieldOpList_eq_sum, WickAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF, WickAlgebra.mem_bosonic_of_mem_free_bosonic, WickAlgebra.timeOrder_timeOrder_right, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_ordered, WickAlgebra.wicks_theorem_normal_order, WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul, WickAlgebra.anPart_mul_anPart_swap, WickContraction.join_timeContract, WickAlgebra.superCommute_anPart_ofFieldOp, WickAlgebra.superCommute_ofFieldOp_ofFieldOpList, WickAlgebra.bosonicProj_bosonicProj_eq_bosonicProj, WickContraction.join_staticContract, WickContraction.staticContract_of_not_gradingCompliant, WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum, WickContraction.wickTerm_empty_nil, WickContraction.timeContract_insert_some_of_lt, 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, WickAlgebra.normalOrder_normalOrder, WickAlgebra.bosonicProj_of_fermionic_part, WickContraction.mul_staticWickTerm_eq_sum, WickAlgebra.ofFieldOpList_eq_ι_ofFieldOpListF, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right, WickAlgebra.superCommute_ofCrAnOp_ofFieldOp_mem_center, 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, 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, WickAlgebra.superCommute_crPart_ofFieldOpList, WickAlgebra.ofFieldOpList_cons, WickContraction.mul_wickTerm_eq_sum, WickAlgebra.timeContract_mem_center, WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_left, WickAlgebra.universalLiftMap_ι, WickContraction.staticWickTerm_empty_nil, WickAlgebra.fermionicProj_of_bosonic_part, WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered, WickAlgebra.normalOrder_uncontracted_none, WickAlgebra.superCommute_ofFieldOpList_ofFieldOp, WickAlgebra.normalOrder_anPart_mul_crPart, WickAlgebra.ofCrAnList_mem_statSubmodule, WickAlgebra.ι_normalOrder_superCommuteF_eq_zero_mul_right, WickAlgebra.normalOrder_superCommute_eq_zero, WickAlgebra.superCommute_create_create, WickAlgebra.ι_superCommuteF_zero_of_fermionic, WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, WickAlgebra.crPart_mul_crPart_swap, WickAlgebra.ι_timeOrderF_superCommuteF_neq_time, WickAlgebra.timeOrder_timeContract_neq_time, WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul, WickAlgebra.ofFieldOp_eq_ι_ofFieldOpF, WickAlgebra.superCommuteRight_apply_ι, WickAlgebra.mem_statSubmodule_of_mem_statisticSubmodule, WickAlgebra.normalOrder_ofFieldOpList_anPart_swap, WickAlgebra.ofFieldOp_mul_ofFieldOp_eq_superCommute, WickContraction.timeContract_of_not_gradingCompliant, WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF, WickAlgebra.universalLift_ι, WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute, WickAlgebra.anPart_inAsymp, WickAlgebra.bosonicProjFree_eq_ι_bosonicProjF, WickAlgebra.anPart_mul_crPart_eq_superCommute, WickAlgebra.fermionicProj_bosonicProj_eq_zero, WickAlgebra.superCommute_anPart_crPart, WickAlgebra.superCommute_ofCrAnOp_ofCrAnList_eq_sum, WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute, WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnListF, WickAlgebra.timeContract_of_timeOrderRel, WickContraction.EqTimeOnly.timeOrder_timeContract_of_not_eqTimeOnly, WickAlgebra.normalOrder_uncontracted_some, WickAlgebra.equiv_iff_sub_mem_ideal, WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_fieldOpFreeAlgebra, WickAlgebra.superCommute_crPart_ofFieldOp, WickAlgebra.normalOrder_ofCrAnOp_ofCrAnList, WickAlgebra.normalOrder_ofCrAnList, WickAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, 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, WickAlgebra.ofCrAnOp_eq_ι_ofCrAnOpF, WickAlgebra.timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, WickAlgebra.bosonicProjFree_eq_of_equiv, 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, WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute, WickAlgebra.timeOrder_timeOrder_mid, WickAlgebra.normalOrder_ofFieldOp_ofFieldOp_swap, WickAlgebra.normalOrder_normalOrder_mid, WickAlgebra.normalOrder_superCommute_mid_eq_zero, WickAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, WickContraction.singleton_staticContract, WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero, WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center, WickAlgebra.ι_eq_zero_iff_mem_ideal, WickAlgebra.crPart_mul_normalOrder, WickAlgebra.ι_superCommuteF_of_create_create, WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, WickAlgebra.ofCrAnList_mem_statSubmodule_of_eq, WickAlgebra.universality, WickAlgebra.ι_timeOrderF_eq_of_equiv, WickAlgebra.timeContract_inAsymp_inAsymp, WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_commute, WickAlgebra.superCommute_annihilate_annihilate, WickAlgebra.crPart_mul_anPart_eq_superCommute, WickContraction.singleton_timeContract, wicks_theorem, WickAlgebra.normalOrder_one_eq_one, WickAlgebra.timeOrder_haveEqTime_split, WickAlgebra.ι_superCommuteF_eq_of_equiv_right, WickAlgebra.timeContract_of_not_timeOrderRel, 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, WickAlgebra.ι_superCommuteF_ofCrAnOpF_superCommuteF_ofCrAnOpF_ofCrAnOpF
|