SuperCommute

📁 Source: PhysLean/QFT/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean

Statistics

Metric	Count
Definitions superCommuteF, «term[_,_]ₛF»	2
Theorems anPartF_mul_anPartF_eq_superCommuteF, anPartF_mul_crPartF_eq_superCommuteF, bonsonic_superCommuteF_symm, bosonic_superCommuteF, crPartF_mul_anPartF_eq_superCommuteF, crPartF_mul_crPartF_eq_superCommuteF, ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF, ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF, ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF, ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF, ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF, ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF, statistic_neq_of_superCommuteF_fermionic, summerCommute_jacobi_ofCrAnListF, superCommuteF_anPartF_anPartF, superCommuteF_anPartF_crPartF, superCommuteF_anPartF_ofFieldOpF, superCommuteF_anPartF_ofFieldOpListF, superCommuteF_bonsonic, superCommuteF_bonsonic_symm, superCommuteF_bosonic_bosonic, superCommuteF_bosonic_fermionic, superCommuteF_bosonic_ofCrAnListF_eq_sum, superCommuteF_crPartF_anPartF, superCommuteF_crPartF_crPartF, superCommuteF_crPartF_ofFieldOpF, superCommuteF_crPartF_ofFieldOpListF, superCommuteF_expand_bosonicProjF_fermionicProjF, superCommuteF_fermionic_bonsonic, superCommuteF_fermionic_fermionic, superCommuteF_fermionic_fermionic_symm, superCommuteF_fermionic_ofCrAnListF_eq_sum, superCommuteF_grade, superCommuteF_ofCrAnListF_ofCrAnListF, superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic, superCommuteF_ofCrAnListF_ofCrAnListF_cons, superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, superCommuteF_ofCrAnListF_ofCrAnListF_symm, superCommuteF_ofCrAnListF_ofFieldOpFsList, superCommuteF_ofCrAnListF_ofFieldOpListF_cons, superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum, superCommuteF_ofCrAnOpF_ofCrAnOpF, superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_fermionic, superCommuteF_ofCrAnOpF_ofCrAnOpF_symm, superCommuteF_ofFieldOpF_ofFieldOpFsList, superCommuteF_ofFieldOpListF_ofFieldOpF, superCommuteF_ofFieldOpListF_ofFieldOpFsList, superCommuteF_superCommuteF_ofCrAnOpF_bosonic_or_fermionic	48
Total	50

FieldSpecification.FieldOpFreeAlgebra

Definitions

Name	Category	Theorems
superCommuteF 📖	CompOp	101 math math: timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_mid, superCommuteF_expand_bosonicProjF_fermionicProjF, superCommuteF_anPartF_crPartF, superCommuteF_crPartF_crPartF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_ofCrAnListF, ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF, superCommuteF_fermionic_fermionic_symm, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel, ofCrAnOpF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.ι_superCommuteF_eq_zero_of_ι_right_zero, normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_left, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_left, superCommuteF_bosonic_fermionic, FieldSpecification.WickAlgebra.superCommuteRight_apply_quot, superCommuteF_crPartF_anPartF, superCommuteF_bosonic_ofCrAnListF_eq_sum, superCommuteF_ofCrAnListF_ofCrAnListF, superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul, superCommuteF_ofCrAnListF_ofFieldOpListF_cons, superCommuteF_ofFieldOpF_ofFieldOpFsList, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_eq_time, FieldSpecification.WickAlgebra.ι_superCommuteF_of_diff_statistic, superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic, crPartF_mul_anPartF_eq_superCommuteF, superCommuteF_crPartF_ofFieldOpListF, ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF, timeOrderF_superCommuteF_ofCrAnOpF_ofCrAnOpF_not_crAnTimeOrderRel_right, superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_fermionic, ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF, superCommuteF_fermionic_fermionic, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul, ofCrAnListF_superCommuteF_normalOrderF_ofCrAnListF, ofCrAnListF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF, superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum, ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF, superCommuteF_anPartF_anPartF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero, ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel, FieldSpecification.WickAlgebra.ι_commute_fieldOpFreeAlgebra_superCommuteF_ofCrAnOpF_ofCrAnOpF, normalOrderF_superCommuteF_crPartF_anPartF, FieldSpecification.WickAlgebra.ι_superCommuteF_of_annihilate_annihilate, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_eq_time, normalOrderF_superCommuteF_create_annihilate, superCommuteF_ofCrAnOpF_ofCrAnOpF_symm, superCommuteF_ofCrAnListF_ofFieldOpFsList, summerCommute_jacobi_ofCrAnListF, anPartF_mul_anPartF_eq_superCommuteF, FieldSpecification.WickAlgebra.ι_superCommuteF_eq_zero_of_ι_left_zero, superCommuteF_anPartF_ofFieldOpListF, FieldSpecification.WickAlgebra.ι_normalOrder_superCommuteF_eq_zero_mul_right, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_neq_time, superCommuteF_anPartF_ofFieldOpF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_eq_zero_mul, superCommuteF_ofFieldOpListF_ofFieldOpFsList, FieldSpecification.WickAlgebra.superCommuteRight_apply_ι, superCommuteF_fermionic_ofCrAnListF_eq_sum, crPartF_mul_crPartF_eq_superCommuteF, superCommuteF_bosonic_bosonic, superCommuteF_ofFieldOpListF_ofFieldOpF, FieldSpecification.WickAlgebra.ι_timeOrderF_superCommuteF_superCommuteF_eq_time_ofCrAnListF, FieldSpecification.WickAlgebra.ι_superCommuteF_right_zero_of_mem_ideal, bosonic_superCommuteF, superCommuteF_ofCrAnOpF_ofCrAnOpF, ofCrAnListF_superCommuteF_normalOrderF_ofFieldOpListF, superCommuteF_ofCrAnListF_ofCrAnListF_symm, superCommuteF_superCommuteF_ofCrAnOpF_bosonic_or_fermionic, superCommuteF_bonsonic_symm, FieldSpecification.WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnListF, timeOrderF_superCommuteF_superCommuteF_ofCrAnOpF_not_crAnTimeOrderRel, anPartF_mul_crPartF_eq_superCommuteF, FieldSpecification.WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_fieldOpFreeAlgebra, normalOrderF_superCommuteF_anPartF_crPartF, bonsonic_superCommuteF_symm, superCommuteF_bonsonic, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_not_crAnTimeOrderRel', FieldSpecification.WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero, superCommuteF_grade, normalOrderF_superCommuteF_annihilate_create, FieldSpecification.WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center, superCommuteF_fermionic_bonsonic, FieldSpecification.WickAlgebra.ι_superCommuteF_of_create_create, superCommuteF_ofCrAnListF_ofCrAnListF_cons, ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF, anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF, superCommuteF_crPartF_ofFieldOpF, FieldSpecification.WickAlgebra.ι_superCommuteF_eq_of_equiv_right, timeOrderF_superCommuteF_ofCrAnOpF_superCommuteF_all_not_crAnTimeOrderRel, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul, FieldSpecification.WickAlgebra.ι_superCommuteF_superCommuteF_ofCrAnOpF_ofCrAnOpF_ofCrAnOpF, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul, FieldSpecification.WickAlgebra.ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul, FieldSpecification.WickAlgebra.superCommute_eq_ι_superCommuteF, FieldSpecification.WickAlgebra.ι_superCommuteF_ofCrAnOpF_superCommuteF_ofCrAnOpF_ofCrAnOpF
«term[_,_]ₛF» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anPartF_mul_anPartF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp anPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic superCommuteF	—	superCommuteF_anPartF_anPartF
anPartF_mul_crPartF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp anPartF crPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic superCommuteF	—	superCommuteF_anPartF_crPartF
bonsonic_superCommuteF_symm 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic	superCommuteF	—	bosonic_superCommuteF superCommuteF_bonsonic
bosonic_superCommuteF 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic	superCommuteF	—	bosonicProjF_add_fermionicProjF superCommuteF_bosonic_bosonic superCommuteF_bosonic_fermionic
crPartF_mul_anPartF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp crPartF anPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic superCommuteF	—	superCommuteF_crPartF_anPartF
crPartF_mul_crPartF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp crPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic superCommuteF	—	superCommuteF_crPartF_crPartF
ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp ofCrAnListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics superCommuteF	—	superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_append
ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp ofCrAnListF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic superCommuteF	—	superCommuteF_ofCrAnListF_ofFieldOpFsList
ofCrAnOpF_mul_ofCrAnListF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp ofCrAnOpF ofCrAnListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList superCommuteF	—	ofCrAnListF_singleton ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF FieldStatistic.ofList_singleton
ofFieldOpF_mul_ofFieldOpListF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp ofFieldOpF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp superCommuteF	—	superCommuteF_ofFieldOpF_ofFieldOpFsList
ofFieldOpListF_mul_ofFieldOpF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp ofFieldOpListF ofFieldOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic superCommuteF	—	superCommuteF_ofFieldOpListF_ofFieldOpF
ofFieldOpListF_mul_ofFieldOpListF_eq_superCommuteF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic superCommuteF	—	superCommuteF_ofFieldOpListF_ofFieldOpFsList
statistic_neq_of_superCommuteF_fermionic 📖	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic superCommuteF ofCrAnListF	—	—	eq_zero_of_bosonic_and_fermionic FieldStatistic.mul_self superCommuteF_grade ofCrAnListF_mem_statisticSubmodule_of
summerCommute_jacobi_ofCrAnListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics	—	superCommuteF_ofCrAnListF_ofCrAnListF FieldStatistic.ofList_append_eq_mul FieldStatistic.mul_self FieldStatistic.bosonic_exchangeSign FieldStatistic.exchangeSign_bosonic FieldStatistic.mul_bosonic FieldStatistic.fermionic_exchangeSign_fermionic
superCommuteF_anPartF_anPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF anPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	anPartF_negAsymp anPartF_position ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofCrAnListF FieldStatistic.ofList_singleton anPartF_posAsymp
superCommuteF_anPartF_crPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF anPartF crPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	anPartF_negAsymp crPartF_posAsymp anPartF_position crPartF_position ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofCrAnListF FieldStatistic.ofList_singleton anPartF_posAsymp crPartF_negAsymp
superCommuteF_anPartF_ofFieldOpF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF anPartF ofFieldOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	ofFieldOpListF_singleton superCommuteF_anPartF_ofFieldOpListF FieldStatistic.ofList_singleton
superCommuteF_anPartF_ofFieldOpListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF anPartF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	anPartF_negAsymp anPartF_position ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofFieldOpFsList FieldStatistic.ofList_singleton anPartF_posAsymp
superCommuteF_bonsonic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic	superCommuteF	—	bosonicProjF_add_fermionicProjF superCommuteF_bosonic_bosonic superCommuteF_fermionic_bonsonic
superCommuteF_bonsonic_symm 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic	superCommuteF	—	bosonic_superCommuteF superCommuteF_bonsonic
superCommuteF_bosonic_bosonic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic	superCommuteF	—	superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_append FieldStatistic.exchangeSign_bosonic
superCommuteF_bosonic_fermionic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic FieldStatistic.fermionic	superCommuteF	—	superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_append FieldStatistic.bosonic_exchangeSign
superCommuteF_bosonic_ofCrAnListF_eq_sum 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic	superCommuteF ofCrAnListF ofCrAnOpF	—	superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum FieldStatistic.bosonic_exchangeSign
superCommuteF_crPartF_anPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF crPartF anPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	crPartF_posAsymp anPartF_negAsymp crPartF_position anPartF_position ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofCrAnListF FieldStatistic.ofList_singleton anPartF_posAsymp crPartF_negAsymp
superCommuteF_crPartF_crPartF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF crPartF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	crPartF_posAsymp crPartF_position ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofCrAnListF FieldStatistic.ofList_singleton crPartF_negAsymp
superCommuteF_crPartF_ofFieldOpF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF crPartF ofFieldOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	ofFieldOpListF_singleton superCommuteF_crPartF_ofFieldOpListF FieldStatistic.ofList_singleton
superCommuteF_crPartF_ofFieldOpListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF crPartF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	crPartF_negAsymp ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofFieldOpFsList FieldStatistic.ofList_singleton crPartF_position crPartF_posAsymp
superCommuteF_expand_bosonicProjF_fermionicProjF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF statisticSubmodule FieldStatistic.bosonic bosonicProjF FieldStatistic.fermionic fermionicProjF	—	bosonicProjF_add_fermionicProjF superCommuteF_bonsonic superCommuteF_fermionic_bonsonic superCommuteF_bosonic_fermionic superCommuteF_fermionic_fermionic
superCommuteF_fermionic_bonsonic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic FieldStatistic.bosonic	superCommuteF	—	superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_append FieldStatistic.exchangeSign_bosonic
superCommuteF_fermionic_fermionic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic	superCommuteF	—	superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_append FieldStatistic.fermionic_exchangeSign_fermionic
superCommuteF_fermionic_fermionic_symm 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic	superCommuteF	—	superCommuteF_fermionic_fermionic
superCommuteF_fermionic_ofCrAnListF_eq_sum 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic	superCommuteF ofCrAnListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics ofCrAnOpF	—	superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum
superCommuteF_grade 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule	FieldStatistic FieldStatistic.instAddMonoid superCommuteF	—	superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_mem_statisticSubmodule_of FieldStatistic.ofList_append_eq_mul
superCommuteF_ofCrAnListF_ofCrAnListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics	—	ofListBasis_eq_ofList
superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic superCommuteF ofCrAnListF FieldStatistic.fermionic	—	FieldStatistic.mul_self superCommuteF_grade ofCrAnListF_mem_statisticSubmodule_of
superCommuteF_ofCrAnListF_ofCrAnListF_cons 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF ofCrAnOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics	—	superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_singleton ofCrAnListF_append FieldStatistic.ofList_singleton ofCrAnListF_cons FieldStatistic.ofList_cons_eq_mul
superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics ofCrAnOpF	—	FieldStatistic.exchangeSign_bosonic ofCrAnListF_nil superCommuteF_ofCrAnListF_ofCrAnListF superCommuteF_ofCrAnListF_ofCrAnListF_cons FieldStatistic.ofList_cons_eq_mul
superCommuteF_ofCrAnListF_ofCrAnListF_symm 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics	—	superCommuteF_ofCrAnListF_ofCrAnListF FieldStatistic.exchangeSign_symm FieldStatistic.exchangeSign_mul_self
superCommuteF_ofCrAnListF_ofFieldOpFsList 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic	—	ofFieldOpListF_sum superCommuteF_ofCrAnListF_ofCrAnListF FieldSpecification.CrAnSection.statistics_eq_state_statistics ofCrAnListF_append
superCommuteF_ofCrAnListF_ofFieldOpListF_cons 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF ofFieldOpListF FieldSpecification.FieldOp ofFieldOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.fieldOpStatistic	—	superCommuteF_ofCrAnListF_ofFieldOpFsList ofFieldOpListF_singleton ofFieldOpListF_append FieldStatistic.ofList_singleton ofFieldOpListF_cons FieldStatistic.ofList_cons_eq_mul
superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnListF ofFieldOpListF FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.fieldOpStatistic ofFieldOpF	—	superCommuteF_ofCrAnListF_ofFieldOpFsList FieldStatistic.exchangeSign_bosonic superCommuteF_ofCrAnListF_ofFieldOpListF_cons FieldStatistic.ofList_cons_eq_mul
superCommuteF_ofCrAnOpF_ofCrAnOpF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics	—	ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofCrAnListF ofCrAnListF_append FieldStatistic.ofList_singleton
superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_fermionic 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic superCommuteF ofCrAnOpF FieldStatistic.fermionic	—	ofCrAnListF_singleton superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic
superCommuteF_ofCrAnOpF_ofCrAnOpF_symm 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofCrAnOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics	—	superCommuteF_ofCrAnOpF_ofCrAnOpF FieldStatistic.exchangeSign_symm FieldStatistic.exchangeSign_mul_self
superCommuteF_ofFieldOpF_ofFieldOpFsList 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofFieldOpF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	ofFieldOpListF_singleton superCommuteF_ofFieldOpListF_ofFieldOpFsList FieldStatistic.ofList_singleton
superCommuteF_ofFieldOpListF_ofFieldOpF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofFieldOpListF ofFieldOpF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic	—	ofFieldOpListF_singleton superCommuteF_ofFieldOpListF_ofFieldOpFsList FieldStatistic.ofList_singleton
superCommuteF_ofFieldOpListF_ofFieldOpFsList 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp superCommuteF ofFieldOpListF FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic	—	ofFieldOpListF_sum superCommuteF_ofCrAnListF_ofFieldOpFsList FieldSpecification.CrAnSection.statistics_eq_state_statistics
superCommuteF_superCommuteF_ofCrAnOpF_bosonic_or_fermionic 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic superCommuteF ofCrAnOpF FieldStatistic.fermionic	—	superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_fermionic ofCrAnOpF_bosonic_or_fermionic FieldStatistic.mul_self superCommuteF_grade

---

← Back to Index