uncontracted 📖 | CompOp | 96 mathmath: wickTerm_insert_some, sign_insert_none_eq_signInsertNone_mul_sign, insertAndContract_uncontractedList_none_zero, sign_insert_none_zero, signFinset_right_map_uncontractedListEmd_eq_filter, staticWickTerm_insert_zero_some, uncontractedList_extractEquiv_symm_none, sign_right_eq_prod_mul_prod, insertAndContractNat_getDualErase, insertLiftSome_bijective, insertAndContract_some_getDual?_self_eq, insertLiftSome_surjective, uncontractedList_extractEquiv_symm_some, insertAndContract_none_succAbove_getDual?_eq_none_iff, insertAndContractNat_some_getDual?_neq_none, insertAndContract_some_getDual?_self_not_none, wickTerm_insert_none, insertAndContractNat_some_getDual?_of_neq, insertAndContract_none_succAbove_getDual?_isSome_iff, uncontractedCongr_none, getDual?_eq_none_iff_mem_uncontracted, uncontractedList_get_mem_uncontracted, timeContract_insert_none, uncontractedList_succAbove_orderedInsert_toFinset, uncontractedList_length_eq_card, insertAndContractNat_succAbove_mem_uncontracted_iff, insertLiftSome_injective, mem_uncontracted_empty, insertAndContract_none_getDual?_self, insertAndContract_some_succAbove_getDual?_eq_option, mem_erase_uncontracted_iff, insertAndContractNat_bijective, uncontractedList_mem_iff, extractEquiv_symm_none_uncontracted, self_mem_uncontracted_of_insertAndContractNat_none, insertAndContract_sndFieldOfContract_some_incl, staticContract_insert_some, insertAndContractNat_some_uncontracted, insertAndContract_isSome_getDual?_self, sum_extractEquiv_congr, mul_staticWickTerm_eq_sum, insertAndContractNat_some_getDual?_eq, uncontractedFieldOpEquiv_list_sum, uncontractedCongr_some, uncontracted_empty, take_uncontractedIndexEquiv_symm, mem_uncontracted_insertAndContractNat_none_iff, insertAndContractNat_injective, mul_wickTerm_eq_sum, insertLift_none_surjective, uncontractedList_toFinset, insertAndContractNat_succAbove_getDual?_isSome_iff, insertAndContract_uncontractedList_none_map, FieldSpecification.WickAlgebra.normalOrder_uncontracted_none, signFinset_insertAndContract_some, insertAndContractNat_succAbove_getDual?_eq_none_iff, insertAndContractNat_none_uncontracted, uncontractedListEmd_mem_uncontracted, uncontractedList_eq_sort, stat_signFinset_insert_some_self_fst, congr_uncontracted, extractEquiv_apply_congr_symm_apply, insertLift_sum, uncontractedList_succAbove_orderedInsert_eq_sort, uncontractedList_getElem_uncontractedIndexEquiv_symm, staticContract_insert_none, insertAndContractNat_none_getDual?_eq_none, insertAndContract_some_prod_contractions, getDualErase_isSome_iff_getDual?_isSome, FieldSpecification.WickAlgebra.normalOrder_uncontracted_some, getDualErase_one, uncontracted_card_eq_iff, sign_insert_some, insertAndContract_some_getDual?_some_eq, self_not_mem_uncontracted_of_insertAndContractNat_some, filter_uncontractedList, timeContract_insertAndContract_some, insertLift_none_bijective, insertAndContractNat_none_getDual?_isNone, uncontracted_card_le, staticWickTerm_insert_zero_none, stat_signFinset_insert_some_self_snd, insertAndContract_none_prod_contractions, insertAndContract_fstFieldOfContract_some_incl, uncontractedList_succAboveEmb_toFinset, insertAndContractNat_some_getDual?_neq_isSome, sign_insert_none, signFinset_insertAndContract_none, uncontractedList_succAboveEmb_eraseIdx_eq_sort, insertAndContractNat_surjective_on_nodual, take_uncontractedListOrderPos_eq_filter_sort, mem_uncontracted_insertAndContractNat_some_iff, uncontractedList_succAboveEmb_eraseIdx_toFinset, mem_uncontracted_iff_not_contracted, uncontractedFieldOpEquiv_none, uncontractedIndexEquiv_symm_eq_filter_length
|