SuperCommute

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

Statistics

Metric	Count
Definitions superCommute, superCommuteRight, «term[_,_]ₛ»	3
Theorems anPart_mul_anPart_swap, anPart_mul_crPart_eq_superCommute, crPart_mul_anPart_eq_superCommute, crPart_mul_crPart_swap, ofCrAnList_mul_ofCrAnList_eq_superCommute, ofCrAnList_mul_ofFieldOpList_eq_superCommute, ofCrAnOp_mul_ofCrAnList_eq_superCommute, ofFieldOpList_mul_ofFieldOpList_eq_superCommute, ofFieldOpList_mul_ofFieldOp_eq_superCommute, ofFieldOp_mul_ofFieldOpList_eq_superCommute, ofFieldOp_mul_ofFieldOp_eq_superCommute, superCommuteRight_apply_quot, superCommuteRight_apply_ι, superCommuteRight_eq_of_equiv, superCommute_anPart_anPart, superCommute_anPart_crPart, superCommute_anPart_ofFieldOp, superCommute_anPart_ofFieldOpF_diff_grade_zero, superCommute_anPart_ofFieldOpList, superCommute_anPart_ofFieldOp_mem_center, superCommute_annihilate_annihilate, superCommute_crPart_anPart, superCommute_crPart_crPart, superCommute_crPart_ofFieldOp, superCommute_crPart_ofFieldOpList, superCommute_create_create, superCommute_diff_statistic, superCommute_eq_ι_superCommuteF, superCommute_ofCrAnList_ofCrAnList, superCommute_ofCrAnList_ofCrAnList_eq_sum, superCommute_ofCrAnList_ofCrAnList_symm, superCommute_ofCrAnList_ofFieldOpList, superCommute_ofCrAnList_ofFieldOpList_eq_sum, superCommute_ofCrAnOp_ofCrAnList_eq_sum, superCommute_ofCrAnOp_ofCrAnOp, superCommute_ofCrAnOp_ofCrAnOp_commute, superCommute_ofCrAnOp_ofCrAnOp_mem_center, superCommute_ofCrAnOp_ofCrAnOp_symm, superCommute_ofCrAnOp_ofFieldOpList_eq_sum, superCommute_ofCrAnOp_ofFieldOp_commute, superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero, superCommute_ofCrAnOp_ofFieldOp_mem_center, superCommute_ofFieldOpList_ofFieldOp, superCommute_ofFieldOpList_ofFieldOpList, superCommute_ofFieldOp_ofFieldOpList, ι_superCommuteF_eq_of_equiv_right, ι_superCommuteF_eq_zero_of_ι_left_zero, ι_superCommuteF_eq_zero_of_ι_right_zero, ι_superCommuteF_right_zero_of_mem_ideal	49
Total	52

FieldSpecification.WickAlgebra

Definitions

Name	Category	Theorems
superCommute 📖	CompOp	59 math math: superCommute_ofCrAnOp_ofCrAnOp, ofFieldOp_mul_ofFieldOpList_eq_superCommute, superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero, ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute, anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder, timeOrder_superCommute_eq_time_left, superCommute_ofCrAnOp_ofCrAnOp_mem_center, timeOrder_superCommute_anPart_ofFieldOp_neq_time, anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, superCommute_ofCrAnOp_ofCrAnOp_symm, superCommute_ofCrAnList_ofCrAnList, ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, normalOrder_superCommute_left_eq_zero, timeOrder_superCommute_eq_time_mid, superCommute_ofCrAnOp_ofFieldOp_commute, anPart_superCommute_normalOrder_ofFieldOpList_sum, timeContract_of_not_timeOrderRel_expand, superCommute_ofFieldOpList_ofFieldOpList, superCommute_ofCrAnList_ofFieldOpList, ofCrAnOp_mul_ofCrAnList_eq_superCommute, superCommute_anPart_ofFieldOp, superCommute_ofFieldOp_ofFieldOpList, superCommute_ofCrAnList_ofFieldOpList_eq_sum, superCommute_anPart_ofFieldOpList, WickContraction.staticContract_insert_some, superCommute_ofCrAnOp_ofFieldOp_mem_center, superCommute_ofCrAnList_ofCrAnList_symm, normalOrder_superCommute_right_eq_zero, timeOrder_superCommute_neq_time, superCommute_crPart_anPart, superCommute_crPart_ofFieldOpList, superCommute_ofFieldOpList_ofFieldOp, normalOrder_superCommute_eq_zero, superCommute_create_create, ofFieldOp_mul_ofFieldOp_eq_superCommute, ofCrAnList_mul_ofCrAnList_eq_superCommute, anPart_mul_crPart_eq_superCommute, superCommute_anPart_crPart, superCommute_ofCrAnOp_ofCrAnList_eq_sum, ofCrAnList_mul_ofFieldOpList_eq_superCommute, timeContract_of_timeOrderRel, superCommute_crPart_ofFieldOp, superCommute_ofCrAnList_ofCrAnList_eq_sum, ofFieldOpList_mul_ofFieldOpList_eq_superCommute, superCommute_anPart_ofFieldOp_mem_center, superCommute_crPart_crPart, superCommute_anPart_ofFieldOpF_diff_grade_zero, superCommute_ofCrAnOp_ofFieldOpList_eq_sum, ofFieldOpList_mul_ofFieldOp_eq_superCommute, normalOrder_superCommute_mid_eq_zero, WickContraction.singleton_staticContract, ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, superCommute_ofCrAnOp_ofCrAnOp_commute, superCommute_annihilate_annihilate, crPart_mul_anPart_eq_superCommute, superCommute_eq_ι_superCommuteF, superCommute_anPart_anPart, superCommute_diff_statistic, timeContract_eq_superCommute
superCommuteRight 📖	CompOp	3 math math: superCommuteRight_apply_quot, superCommuteRight_eq_of_equiv, superCommuteRight_apply_ι
«term[_,_]ₛ» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anPart_mul_anPart_swap 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet anPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	anPart.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_anPartF superCommute_anPart_anPart
anPart_mul_crPart_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet anPart crPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic superCommute	—	superCommute_anPart_crPart
crPart_mul_anPart_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet crPart anPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic superCommute	—	superCommute_crPart_anPart
crPart_mul_crPart_swap 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet crPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	crPart.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_crPartF superCommute_crPart_crPart
ofCrAnList_mul_ofCrAnList_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofCrAnList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics superCommute	—	superCommute_ofCrAnList_ofCrAnList ofCrAnList_append
ofCrAnList_mul_ofFieldOpList_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofCrAnList ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic superCommute	—	superCommute_ofCrAnList_ofFieldOpList
ofCrAnOp_mul_ofCrAnList_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofCrAnOp ofCrAnList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList superCommute	—	ofCrAnList_singleton ofCrAnList_mul_ofCrAnList_eq_superCommute FieldStatistic.ofList_singleton
ofFieldOpList_mul_ofFieldOpList_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic superCommute	—	superCommute_ofFieldOpList_ofFieldOpList
ofFieldOpList_mul_ofFieldOp_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofFieldOpList ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic superCommute	—	superCommute_ofFieldOpList_ofFieldOp
ofFieldOp_mul_ofFieldOpList_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofFieldOp ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp superCommute	—	superCommute_ofFieldOp_ofFieldOpList
ofFieldOp_mul_ofFieldOp_eq_superCommute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic superCommute	—	ofFieldOpList_singleton ofFieldOpList_mul_ofFieldOpList_eq_superCommute FieldStatistic.ofList_singleton
superCommuteRight_apply_quot 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommuteRight ι FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	—
superCommuteRight_apply_ι 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommuteRight ι FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	—
superCommuteRight_eq_of_equiv 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra instSetoidFieldOpFreeAlgebra	superCommuteRight	—	ι_surjective superCommuteRight_apply_ι ι_superCommuteF_eq_zero_of_ι_left_zero ι_eq_zero_iff_mem_ideal equiv_iff_sub_mem_ideal
superCommute_anPart_anPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart	—	anPart_inAsymp anPart_position superCommute_annihilate_annihilate anPart_outAsymp
superCommute_anPart_crPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart crPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	anPart.eq_1 crPart.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_crPartF
superCommute_anPart_ofFieldOp 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	anPart.eq_1 ofFieldOp.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpF
superCommute_anPart_ofFieldOpF_diff_grade_zero 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart ofFieldOp	—	anPart_inAsymp superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero
superCommute_anPart_ofFieldOpList 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	anPart.eq_1 ofFieldOpList.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_anPartF_ofFieldOpListF
superCommute_anPart_ofFieldOp_mem_center 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute anPart ofFieldOp	—	anPart_inAsymp superCommute_ofCrAnOp_ofFieldOp_mem_center
superCommute_annihilate_annihilate 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.annihilate	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp	—	ofCrAnOp.eq_1 superCommute_eq_ι_superCommuteF ι_superCommuteF_of_annihilate_annihilate
superCommute_crPart_anPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute crPart anPart FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	anPart.eq_1 crPart.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_anPartF
superCommute_crPart_crPart 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute crPart	—	crPart_outAsymp crPart_position superCommute_create_create crPart_inAsymp
superCommute_crPart_ofFieldOp 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute crPart ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic	—	crPart.eq_1 ofFieldOp.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpF
superCommute_crPart_ofFieldOpList 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute crPart ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	crPart.eq_1 ofFieldOpList.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_crPartF_ofFieldOpListF
superCommute_create_create 📖	mathematical	FieldSpecification.crAnFieldOpToCreateAnnihilate CreateAnnihilate.create	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp	—	ofCrAnOp.eq_1 superCommute_eq_ι_superCommuteF ι_superCommuteF_of_create_create
superCommute_diff_statistic 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp	—	ofCrAnOp.eq_1 superCommute_eq_ι_superCommuteF ι_superCommuteF_of_diff_statistic
superCommute_eq_ι_superCommuteF 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ι FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	—
superCommute_ofCrAnList_ofCrAnList 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics	—	ofCrAnList_eq_ι_ofCrAnListF superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF
superCommute_ofCrAnList_ofCrAnList_eq_sum 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics ofCrAnOp	—	ofCrAnList.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum
superCommute_ofCrAnList_ofCrAnList_symm 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics	—	ofCrAnList.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_symm
superCommute_ofCrAnList_ofFieldOpList 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnList ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic	—	ofCrAnList.eq_1 ofFieldOpList.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpFsList
superCommute_ofCrAnList_ofFieldOpList_eq_sum 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnList ofFieldOpList FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.crAnStatistics FieldSpecification.fieldOpStatistic ofFieldOp	—	ofCrAnList.eq_1 ofFieldOpList.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum
superCommute_ofCrAnOp_ofCrAnList_eq_sum 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp ofCrAnList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList	—	ofCrAnList_singleton superCommute_ofCrAnList_ofCrAnList_eq_sum FieldStatistic.ofList_singleton superCommute_ofCrAnOp_ofCrAnOp_commute ofCrAnList_append
superCommute_ofCrAnOp_ofCrAnOp 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics	—	ofCrAnOp.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF
superCommute_ofCrAnOp_ofCrAnOp_commute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp	—	superCommute_ofCrAnOp_ofCrAnOp_mem_center
superCommute_ofCrAnOp_ofCrAnOp_mem_center 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp	—	ofCrAnOp.eq_1 superCommute_eq_ι_superCommuteF ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center
superCommute_ofCrAnOp_ofCrAnOp_symm 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics	—	ofCrAnOp.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnOpF_ofCrAnOpF_symm
superCommute_ofCrAnOp_ofFieldOpList_eq_sum 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp ofFieldOpList FieldSpecification.FieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.crAnStatistics FieldStatistic.ofList FieldSpecification.fieldOpStatistic ofFieldOp	—	ofCrAnList_singleton superCommute_ofCrAnList_ofFieldOpList_eq_sum FieldStatistic.ofList_singleton superCommute_ofCrAnOp_ofFieldOp_commute ofFieldOpList_append
superCommute_ofCrAnOp_ofFieldOp_commute 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp ofFieldOp	—	superCommute_ofCrAnOp_ofFieldOp_mem_center
superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp ofFieldOp	—	ofFieldOp_eq_sum superCommute_diff_statistic
superCommute_ofCrAnOp_ofFieldOp_mem_center 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofCrAnOp ofFieldOp	—	ofFieldOp_eq_sum superCommute_ofCrAnOp_ofCrAnOp_mem_center
superCommute_ofFieldOpList_ofFieldOp 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofFieldOpList ofFieldOp FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic	—	ofFieldOpList.eq_1 ofFieldOp.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpF
superCommute_ofFieldOpList_ofFieldOpList 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldStatistic.ofList FieldSpecification.FieldOp FieldSpecification.fieldOpStatistic	—	ofFieldOpList.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpListF_ofFieldOpFsList
superCommute_ofFieldOp_ofFieldOpList 📖	mathematical	—	FieldSpecification.WickAlgebra FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet superCommute ofFieldOp ofFieldOpList FieldStatistic FieldStatistic.instCommGroup FieldStatistic.exchangeSign FieldSpecification.fieldOpStatistic FieldStatistic.ofList FieldSpecification.FieldOp	—	ofFieldOp.eq_1 ofFieldOpList.eq_1 superCommute_eq_ι_superCommuteF FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofFieldOpF_ofFieldOpFsList
ι_superCommuteF_eq_of_equiv_right 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra instSetoidFieldOpFreeAlgebra	FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	ι_superCommuteF_right_zero_of_mem_ideal equiv_iff_sub_mem_ideal
ι_superCommuteF_eq_zero_of_ι_left_zero 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι	FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	FieldSpecification.FieldOpFreeAlgebra.superCommuteF_expand_bosonicProjF_fermionicProjF ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero
ι_superCommuteF_eq_zero_of_ι_right_zero 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι	FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	FieldSpecification.FieldOpFreeAlgebra.superCommuteF_expand_bosonicProjF_fermionicProjF ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero
ι_superCommuteF_right_zero_of_mem_ideal 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet	FieldSpecification.WickAlgebra ι FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	ι_superCommuteF_eq_zero_of_ι_right_zero ι_eq_zero_iff_mem_ideal

---

← Back to Index