Basic

📁 Source: PhysLean/QFT/PerturbationTheory/FieldStatistics/Basic.lean

Statistics

Metric	Count
Definitions FieldStatistic, instAddMonoid, instCommGroup, instFintype, ofList, instDecidableEqFieldStatistic	6
Theorems add_eq_mul, bonsic_eq_fermionic_false, bosonic_mul_bosonic, bosonic_mul_fermionic, bosonic_neq_iff_fermionic_eq, eq_self_if_bosonic_eq, eq_self_if_eq_bosonic, fermionic_mul_bosonic, fermionic_mul_fermionic, fermionic_neq_iff_bosonic_eq, fermionic_not_eq_bonsic, mul_bosonic, mul_eq_iff_eq_mul, mul_eq_iff_eq_mul', mul_eq_one_iff, mul_self, neq_bosonic_iff_eq_fermionic, neq_fermionic_iff_eq_bosonic, ofList_append, ofList_append_eq_mul, ofList_cons_eq_mul, ofList_empty, ofList_eq_prod, ofList_freeMonoid, ofList_insert_lt_eq, ofList_insertionSort, ofList_map_eq_finset_prod, ofList_orderedInsert, ofList_pair, ofList_perm, ofList_singleton, ofList_take_eraseIdx, ofList_take_insert, ofList_take_insertIdx_gt, ofList_take_insertIdx_le, ofList_take_succ_cons, ofList_take_zero, one_eq_mul_iff	38
Total	44

FieldStatistic

Definitions

Name	Category	Theorems
instAddMonoid 📖	CompOp	2 math math: add_eq_mul, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_grade
instCommGroup 📖	CompOp	175 math math: FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp, FieldSpecification.WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder, WickContraction.wickTerm_insert_some, add_eq_mul, FieldSpecification.WickAlgebra.normalOrder_ofFieldOp_mul_ofFieldOp, WickContraction.staticContract_insert_some_of_lt, Wick.koszulSign_eraseIdx_insertionSortMinPos, FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_crPartF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_crPartF, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul, ofList_take_zero, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF, fermionic_mul_bosonic, WickContraction.sign_right_eq_prod_mul_prod, mul_eq_iff_eq_mul, WickContraction.join_singleton_sign_right, ofList_take_succ_cons, Wick.koszulSignInsert_eq_exchangeSign_take, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset, WickContraction.signInsertSomeProd_eq_prod_fin, FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.ofFieldOpList_normalOrder_insert, FieldSpecification.WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_crPartF_anPartF, FieldSpecification.normalOrderSign_swap_create_annihilate_fst, ofFinset_empty, WickContraction.wickTerm_insert_none, WickContraction.signInsertSomeCoef_eq_finset, FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_symm, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList, ofFinset_union_disjoint, ofFinset_union, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered, ofList_eq_prod, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_anPartF, FieldSpecification.WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, WickContraction.signInsertSome_mul_filter_contracted_of_lt, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF, ofFinset_eq_prod, mul_bosonic, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, WickContraction.signInsertSomeProd_eq_finset, WickContraction.sign_insert_some_of_not_lt, ofList_pair, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_cons, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpF_ofFieldOpFsList, WickContraction.signInsertNone_eq_filter_map, FieldSpecification.WickAlgebra.anPart_superCommute_normalOrder_ofFieldOpList_sum, FieldSpecification.WickAlgebra.timeOrder_eq_maxTimeField_mul_finset, exchangeSign_mul_self_swap, ofFinset_erase, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF, exchangeSign_bosonic, FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel_expand, FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList, WickContraction.timeContract_insert_some_of_not_lt, FieldSpecification.FieldOpFreeAlgebra.crPartF_mul_anPartF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpListF, ofFinset_insert, FieldSpecification.WickAlgebra.ofCrAnOp_mul_ofCrAnList_eq_superCommute, FieldSpecification.WickAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_anPartF_mul_crPartF, WickContraction.join_singleton_sign_left, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_anPartF_crPartF, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF, WickContraction.signInsertSomeCoef_if, FieldSpecification.WickAlgebra.anPart_mul_anPart_swap, FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOp, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.superCommute_ofFieldOp_ofFieldOpList, FieldSpecification.normalOrderSign_swap_create_annihilate, WickContraction.signInsertSomeProd_eq_one_if, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF, WickContraction.sign_insert_some_zero, FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum, WickContraction.timeContract_insert_some_of_lt, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_anPartF, FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpList, WickContraction.joinSignRightExtra_eq_i_j_finset_eq_if, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF, ofList_append_eq_mul, WickContraction.signInsertSome_mul_filter_contracted_of_not_lt, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_symm, exchangeSign_ofList_cons, mul_self, FieldSpecification.WickAlgebra.superCommute_crPart_anPart, FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOpList, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_symm, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate, exchangeSign_cocycle, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpFsList, mul_eq_one_iff, FieldSpecification.FieldOpFreeAlgebra.summerCommute_jacobi_ofCrAnListF, WickContraction.mul_wickTerm_eq_sum, FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_anPartF_eq_superCommuteF, FieldSpecification.WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered, FieldSpecification.WickAlgebra.normalOrder_uncontracted_none, FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOp, mul_eq_iff_eq_mul', FieldSpecification.WickAlgebra.normalOrder_anPart_mul_crPart, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpListF, exchangeSign_symm, ofFinset_filter, FieldSpecification.koszulSignInsert_annihilate_cons_create, ofList_take_insertIdx_le, FieldSpecification.WickAlgebra.crPart_mul_crPart_swap, WickContraction.stat_ofFinset_eq_one_of_gradingCompliant, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpF, bosonic_mul_fermionic, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList, FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_anPart_swap, WickContraction.signInsertNone_eq_prod_getDual?_Some, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_fermionic_ofCrAnListF_eq_sum, fermionic_mul_fermionic, FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOp_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.crPartF_mul_crPartF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpF, exchangeSign_mul_self, FieldSpecification.timeOrderSign_pair_not_ordered, Wick.koszulSign_eraseIdx, ofList_map_eq_finset_prod, FieldSpecification.WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofFieldOpF_mul_ofFieldOpF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF, FieldSpecification.WickAlgebra.anPart_mul_crPart_eq_superCommute, FieldSpecification.WickAlgebra.superCommute_anPart_crPart, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_symm, FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnList_eq_sum, FieldSpecification.WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute, FieldSpecification.timerOrderSign_of_eraseMaxTimeField, WickContraction.singleton_sign_expand, FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_crPartF_eq_superCommuteF, FieldSpecification.crAnTimeOrderSign_pair_not_ordered, bosonic_exchangeSign, FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOp, WickContraction.signInsertNone_eq_prod_prod, FieldSpecification.WickAlgebra.normalOrder_ofCrAnOp_ofCrAnList, Wick.koszulSignCons_eq_exchangeSign, WickContraction.join_singleton_left_signFinset_eq_filter, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_eq_sum, FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOpList_eq_superCommute, FieldSpecification.WickAlgebra.normalOrder_anPart_ofFieldOpList_swap, FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_mul_anPart_swap, WickContraction.signInsertNone_eq_filterset, FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofFieldOpList_eq_sum, WickContraction.signInsertSomeProd_eq_prod_prod, FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute, FieldSpecification.WickAlgebra.normalOrder_ofFieldOp_ofFieldOp_swap, bosonic_mul_bosonic, exchangeSign_eq_if, WickContraction.sign_insert_some_of_lt, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_cons, FieldSpecification.WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, WickContraction.sign_insert_none, Wick.koszulSign_insertIdx, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF, FieldSpecification.normalOrderSign_eraseIdx, FieldSpecification.WickAlgebra.crPart_mul_anPart_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, ofList_cons_eq_mul, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpF, FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel, fermionic_exchangeSign_fermionic, WickContraction.signInsertNone_eq_mul_fst_snd, one_eq_mul_iff, ofFinset_filter_mul_neg, FieldSpecification.WickAlgebra.timeContract_eq_superCommute
instFintype 📖	CompOp	—
ofList 📖	CompOp	89 math math: Wick.koszulSign_eraseIdx_insertionSortMinPos, FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute, ofList_empty, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul, ofList_take_zero, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF, ofList_take_succ_cons, Wick.koszulSignInsert_eq_exchangeSign_take, ofList_take_insertIdx_gt, FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.ofFieldOpList_normalOrder_insert, FieldSpecification.WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, ofList_insert_lt_eq, ofList_freeMonoid, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList, Wick.koszulSignInsert_eq_grade, ofList_eq_prod, FieldSpecification.WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, ofList_pair, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_cons, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpF_ofFieldOpFsList, WickContraction.signInsertNone_eq_filter_map, FieldSpecification.WickAlgebra.anPart_superCommute_normalOrder_ofFieldOpList_sum, ofList_take_eraseIdx, FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpListF, FieldSpecification.WickAlgebra.ofCrAnOp_mul_ofCrAnList_eq_superCommute, FieldSpecification.WickAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.superCommute_ofFieldOp_ofFieldOpList, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum, FieldSpecification.CrAnSection.take_statistics_eq_take_state_statistics, FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum, FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpList, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF, ofList_append_eq_mul, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_symm, exchangeSign_ofList_cons, FieldSpecification.CrAnSection.statistics_eq_state_statistics, ofList_singleton, FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOpList, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpFsList, FieldSpecification.FieldOpFreeAlgebra.summerCommute_jacobi_ofCrAnListF, FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOp, ofList_append, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpListF, FieldSpecification.WickAlgebra.ofCrAnList_mem_statSubmodule, ofList_take_insertIdx_le, FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF_if_bosonic, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList, FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_anPart_swap, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_fermionic_ofCrAnListF_eq_sum, ofList_insertionSort, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpF, Wick.koszulSign_eraseIdx, ofList_map_eq_finset_prod, FieldSpecification.WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute, ofList_perm, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_symm, FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnList_eq_sum, FieldSpecification.WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute, FieldSpecification.timerOrderSign_of_eraseMaxTimeField, FieldSpecification.WickAlgebra.normalOrder_ofCrAnOp_ofCrAnList, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_eq_sum, FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOpList_eq_superCommute, FieldSpecification.WickAlgebra.normalOrder_anPart_ofFieldOpList_swap, ofList_orderedInsert, FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_mul_anPart_swap, FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofFieldOpList_eq_sum, FieldSpecification.normalOrderList_statistics, FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_cons, FieldSpecification.WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, ofList_take_insert, Wick.koszulSign_insertIdx, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF, FieldSpecification.normalOrderSign_eraseIdx, FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_ofCrAnListF, FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, ofList_cons_eq_mul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_mul 📖	mathematical	—	FieldStatistic instAddMonoid instCommGroup	—	—
bonsic_eq_fermionic_false 📖	mathematical	—	bosonic fermionic	—	—
bosonic_mul_bosonic 📖	mathematical	—	FieldStatistic instCommGroup bosonic	—	—
bosonic_mul_fermionic 📖	mathematical	—	FieldStatistic instCommGroup bosonic fermionic	—	—
bosonic_neq_iff_fermionic_eq 📖	mathematical	—	bosonic fermionic	—	—
eq_self_if_bosonic_eq 📖	mathematical	—	FieldStatistic bosonic instDecidableEqFieldStatistic fermionic	—	—
eq_self_if_eq_bosonic 📖	mathematical	—	FieldStatistic bosonic instDecidableEqFieldStatistic fermionic	—	—
fermionic_mul_bosonic 📖	mathematical	—	FieldStatistic instCommGroup fermionic bosonic	—	—
fermionic_mul_fermionic 📖	mathematical	—	FieldStatistic instCommGroup fermionic bosonic	—	—
fermionic_neq_iff_bosonic_eq 📖	mathematical	—	fermionic bosonic	—	—
fermionic_not_eq_bonsic 📖	mathematical	—	fermionic bosonic	—	—
mul_bosonic 📖	mathematical	—	FieldStatistic instCommGroup bosonic	—	—
mul_eq_iff_eq_mul 📖	mathematical	—	FieldStatistic instCommGroup	—	mul_self
mul_eq_iff_eq_mul' 📖	mathematical	—	FieldStatistic instCommGroup	—	mul_self
mul_eq_one_iff 📖	mathematical	—	FieldStatistic instCommGroup	—	mul_self mul_bosonic
mul_self 📖	mathematical	—	FieldStatistic instCommGroup	—	—
neq_bosonic_iff_eq_fermionic 📖	mathematical	—	bosonic fermionic	—	—
neq_fermionic_iff_eq_bosonic 📖	mathematical	—	fermionic bosonic	—	—
ofList_append 📖	mathematical	—	ofList FieldStatistic instDecidableEqFieldStatistic bosonic fermionic	—	eq_self_if_bosonic_eq
ofList_append_eq_mul 📖	mathematical	—	ofList FieldStatistic instCommGroup	—	ofList_append
ofList_cons_eq_mul 📖	mathematical	—	ofList FieldStatistic instCommGroup	—	—
ofList_empty 📖	mathematical	—	ofList bosonic	—	—
ofList_eq_prod 📖	mathematical	—	ofList FieldStatistic instCommGroup	—	ofList_cons_eq_mul
ofList_freeMonoid 📖	mathematical	—	ofList	—	ofList_singleton
ofList_insert_lt_eq 📖	mathematical	—	ofList	—	ofList_perm PhysLean.List.take_insert_let
ofList_insertionSort 📖	mathematical	—	ofList	—	ofList_perm
ofList_map_eq_finset_prod 📖	mathematical	—	ofList FieldStatistic instCommGroup	—	—
ofList_orderedInsert 📖	mathematical	—	ofList	—	ofList_perm
ofList_pair 📖	mathematical	—	ofList FieldStatistic instCommGroup	—	ofList_cons_eq_mul ofList_singleton
ofList_perm 📖	mathematical	—	ofList	—	ofList_eq_prod
ofList_singleton 📖	mathematical	—	ofList	—	eq_self_if_eq_bosonic
ofList_take_eraseIdx 📖	mathematical	—	ofList	—	PhysLean.List.take_eraseIdx_same
ofList_take_insert 📖	mathematical	—	ofList	—	PhysLean.List.take_insert_same
ofList_take_insertIdx_gt 📖	mathematical	—	ofList	—	PhysLean.List.take_insert_gt
ofList_take_insertIdx_le 📖	mathematical	—	ofList FieldStatistic instCommGroup	—	ofList_insert_lt_eq ofList_take_succ_cons
ofList_take_succ_cons 📖	mathematical	—	ofList FieldStatistic instCommGroup	—	ofList_cons_eq_mul
ofList_take_zero 📖	mathematical	—	ofList FieldStatistic instCommGroup	—	—
one_eq_mul_iff 📖	mathematical	—	FieldStatistic instCommGroup	—	mul_self mul_bosonic

(root)

Definitions

Name	Category	Theorems
FieldStatistic 📖	CompData	195 math math: FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp, FieldSpecification.WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered_eq_timeOrder, WickContraction.wickTerm_insert_some, FieldStatistic.add_eq_mul, FieldSpecification.WickAlgebra.normalOrder_ofFieldOp_mul_ofFieldOp, WickContraction.staticContract_insert_some_of_lt, Wick.koszulSign_eraseIdx_insertionSortMinPos, FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOpList_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_crPartF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_crPartF, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul, FieldStatistic.eq_self_if_eq_bosonic, FieldStatistic.ofList_take_zero, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF, FieldStatistic.fermionic_mul_bosonic, WickContraction.sign_right_eq_prod_mul_prod, FieldStatistic.mul_eq_iff_eq_mul, WickContraction.join_singleton_sign_right, FieldStatistic.ofList_take_succ_cons, FieldSpecification.WickAlgebra.bosonicProj_of_bosonic_part, Wick.koszulSignInsert_eq_exchangeSign_take, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset, WickContraction.signInsertSomeProd_eq_prod_fin, FieldSpecification.FieldOpFreeAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.ofFieldOpList_normalOrder_insert, FieldSpecification.WickAlgebra.anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_crPartF_anPartF, FieldSpecification.normalOrderSign_swap_create_annihilate_fst, FieldStatistic.ofFinset_empty, WickContraction.wickTerm_insert_none, WickContraction.signInsertSomeCoef_eq_finset, FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnOp_symm, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList, FieldStatistic.ofFinset_union_disjoint, FieldStatistic.ofFinset_union, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered, Wick.koszulSignInsert_eq_grade, FieldStatistic.ofList_eq_prod, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_anPartF, FieldSpecification.WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, WickContraction.signInsertSome_mul_filter_contracted_of_lt, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF, FieldStatistic.ofFinset_eq_prod, FieldSpecification.FieldOpFreeAlgebra.directSum_eq_bosonic_plus_fermionic, FieldStatistic.mul_bosonic, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, WickContraction.signInsertSomeProd_eq_finset, WickContraction.sign_insert_some_of_not_lt, FieldStatistic.ofList_pair, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_cons, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpF_ofFieldOpFsList, WickContraction.signInsertNone_eq_filter_map, FieldSpecification.WickAlgebra.anPart_superCommute_normalOrder_ofFieldOpList_sum, FieldSpecification.WickAlgebra.timeOrder_eq_maxTimeField_mul_finset, FieldStatistic.exchangeSign_mul_self_swap, FieldStatistic.ofFinset_erase, FieldSpecification.FieldOpFreeAlgebra.timeOrderF_ofFieldOpF_ofFieldOpF_not_ordered_eq_timeOrderF, FieldStatistic.exchangeSign_bosonic, FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel_expand, FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOpList, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList, WickContraction.timeContract_insert_some_of_not_lt, FieldSpecification.FieldOpFreeAlgebra.crPartF_mul_anPartF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpListF, FieldStatistic.ofFinset_insert, FieldSpecification.WickAlgebra.ofCrAnOp_mul_ofCrAnList_eq_superCommute, FieldSpecification.WickAlgebra.normalOrder_ofCrAnOp_ofFieldOpList_swap, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_anPartF_mul_crPartF, WickContraction.join_singleton_sign_left, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_anPartF_crPartF, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF, WickContraction.signInsertSomeCoef_if, FieldSpecification.WickAlgebra.anPart_mul_anPart_swap, FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOp, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.superCommute_ofFieldOp_ofFieldOpList, FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_fermionic_part, FieldSpecification.normalOrderSign_swap_create_annihilate, WickContraction.signInsertSomeProd_eq_one_if, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate_ofCrAnListF_ofCrAnListF, WickContraction.sign_insert_some_zero, FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofFieldOpList_eq_sum, WickContraction.timeContract_insert_some_of_lt, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_anPartF, FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpList, FieldSpecification.WickAlgebra.fermionicProj_of_fermionic_part, WickContraction.joinSignRightExtra_eq_i_j_finset_eq_if, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF, FieldSpecification.WickAlgebra.bosonicProj_of_fermionic_part, FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF, FieldStatistic.ofList_append_eq_mul, WickContraction.signInsertSome_mul_filter_contracted_of_not_lt, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_symm, FieldStatistic.exchangeSign_ofList_cons, FieldStatistic.mul_self, FieldSpecification.WickAlgebra.superCommute_crPart_anPart, FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOpList, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_symm, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_swap_create_annihilate, FieldStatistic.exchangeSign_cocycle, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpFsList, FieldStatistic.mul_eq_one_iff, FieldSpecification.FieldOpFreeAlgebra.summerCommute_jacobi_ofCrAnListF, WickContraction.mul_wickTerm_eq_sum, FieldStatistic.eq_self_if_bosonic_eq, FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_anPartF_eq_superCommuteF, FieldSpecification.WickAlgebra.fermionicProj_of_bosonic_part, FieldSpecification.WickAlgebra.timeOrder_ofFieldOp_ofFieldOp_not_ordered, FieldSpecification.WickAlgebra.normalOrder_uncontracted_none, FieldSpecification.WickAlgebra.superCommute_ofFieldOpList_ofFieldOp, FieldStatistic.ofList_append, FieldStatistic.mul_eq_iff_eq_mul', FieldSpecification.WickAlgebra.normalOrder_anPart_mul_crPart, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpListF, FieldStatistic.exchangeSign_symm, FieldStatistic.ofFinset_filter, FieldSpecification.koszulSignInsert_annihilate_cons_create, FieldStatistic.ofList_take_insertIdx_le, FieldSpecification.WickAlgebra.crPart_mul_crPart_swap, WickContraction.stat_ofFinset_eq_one_of_gradingCompliant, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpF, FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF_if_bosonic, FieldStatistic.bosonic_mul_fermionic, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList, FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_anPart_swap, WickContraction.signInsertNone_eq_prod_getDual?_Some, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_fermionic_ofCrAnListF_eq_sum, FieldStatistic.fermionic_mul_fermionic, FieldSpecification.WickAlgebra.ofFieldOp_mul_ofFieldOp_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.crPartF_mul_crPartF_eq_superCommuteF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpF, FieldStatistic.exchangeSign_mul_self, FieldSpecification.timeOrderSign_pair_not_ordered, Wick.koszulSign_eraseIdx, FieldStatistic.ofList_map_eq_finset_prod, FieldSpecification.WickAlgebra.ofCrAnList_mul_ofCrAnList_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.normalOrderF_ofFieldOpF_mul_ofFieldOpF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF, FieldSpecification.WickAlgebra.anPart_mul_crPart_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_bosonic_part, FieldSpecification.WickAlgebra.superCommute_anPart_crPart, FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_symm, FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofCrAnList_eq_sum, FieldSpecification.WickAlgebra.ofCrAnList_mul_ofFieldOpList_eq_superCommute, FieldSpecification.timerOrderSign_of_eraseMaxTimeField, WickContraction.singleton_sign_expand, FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_bonosic_part, FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_crPartF_eq_superCommuteF, FieldSpecification.crAnTimeOrderSign_pair_not_ordered, FieldStatistic.bosonic_exchangeSign, FieldSpecification.WickAlgebra.superCommute_crPart_ofFieldOp, WickContraction.signInsertNone_eq_prod_prod, FieldSpecification.WickAlgebra.normalOrder_ofCrAnOp_ofCrAnList, Wick.koszulSignCons_eq_exchangeSign, WickContraction.join_singleton_left_signFinset_eq_filter, FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_fermionic_part, FieldSpecification.WickAlgebra.superCommute_ofCrAnList_ofCrAnList_eq_sum, FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOpList_eq_superCommute, FieldSpecification.WickAlgebra.directSum_eq_bosonic_plus_fermionic, FieldSpecification.WickAlgebra.normalOrder_anPart_ofFieldOpList_swap, FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_mul_anPart_swap, WickContraction.signInsertNone_eq_filterset, FieldSpecification.WickAlgebra.superCommute_ofCrAnOp_ofFieldOpList_eq_sum, WickContraction.signInsertSomeProd_eq_prod_prod, FieldSpecification.WickAlgebra.ofFieldOpList_mul_ofFieldOp_eq_superCommute, FieldSpecification.WickAlgebra.normalOrder_ofFieldOp_ofFieldOp_swap, FieldStatistic.bosonic_mul_bosonic, FieldSpecification.WickAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_grade, FieldStatistic.exchangeSign_eq_if, WickContraction.sign_insert_some_of_lt, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_cons, FieldSpecification.WickAlgebra.ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, WickContraction.sign_insert_none, Wick.koszulSign_insertIdx, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF, FieldSpecification.normalOrderSign_eraseIdx, FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_ofCrAnListF, FieldSpecification.WickAlgebra.crPart_mul_anPart_eq_superCommute, FieldSpecification.FieldOpFreeAlgebra.anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldStatistic.ofList_cons_eq_mul, FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpF, FieldSpecification.WickAlgebra.timeContract_of_not_timeOrderRel, FieldStatistic.fermionic_exchangeSign_fermionic, WickContraction.signInsertNone_eq_mul_fst_snd, FieldStatistic.one_eq_mul_iff, FieldStatistic.ofFinset_filter_mul_neg, FieldSpecification.WickAlgebra.timeContract_eq_superCommute
instDecidableEqFieldStatistic 📖	CompOp	12 math math: FieldStatistic.eq_self_if_eq_bosonic, FieldSpecification.FieldOpFreeAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, Wick.koszulSignInsert_eq_grade, FieldSpecification.FieldOpFreeAlgebra.directSum_eq_bosonic_plus_fermionic, FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF, FieldStatistic.eq_self_if_bosonic_eq, FieldStatistic.ofList_append, FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_ofCrAnListF_if_bosonic, FieldSpecification.WickAlgebra.directSum_eq_bosonic_plus_fermionic, FieldSpecification.WickAlgebra.coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, FieldStatistic.exchangeSign_eq_if, FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_ofCrAnListF

---

← Back to Index