Basic

📁 Source: PhysLean/QFT/PerturbationTheory/WickAlgebra/NormalOrder/Basic.lean

Statistics

Metric	Count
Definitions normalOrder, «term𝓝(_)»»)	2
Theorems ι_normalOrderF_eq_of_equiv, ι_normalOrderF_superCommuteF_eq_zero, ι_normalOrderF_superCommuteF_eq_zero_mul, ι_normalOrderF_superCommuteF_eq_zero_mul_left, ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right, ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero, ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul, ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero, ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul, ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul, ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul, ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul, ι_normalOrderF_zero_of_mem_ideal, ι_normalOrder_superCommuteF_eq_zero_mul_right	14
Total	16

FieldSpecification.WickAlgebra

Definitions

Name	Category	Theorems
normalOrder 📖	CompOp	50 math math: WickContraction.wickTerm_insert_some, timeContract_eq_smul, normalOrder_ofFieldOp_mul_ofFieldOp, normalOrder_ofCrAnList_nil, ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute, WickContraction.staticWickTerm_insert_zero_some, anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder, normalOrder_normalOrder_right, wicks_theorem_normal_order_empty, normalOrder_anPart_mul_anPart, normalOrder_ofFieldOpList_nil, ofFieldOpList_normalOrder_insert, anPart_mul_normalOrder_ofFieldOpList_eq_superCommute, WickContraction.wickTerm_insert_none, normalOrder_eq_ι_normalOrderF, ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, normalOrder_superCommute_left_eq_zero, anPart_superCommute_normalOrder_ofFieldOpList_sum, ofCrAnList_eq_normalOrder, normalOrder_crPart_mul_crPart, normalOrder_crPart_mul_anPart, normalOrder_ofCrAnOp_ofFieldOpList_swap, wicks_theorem_normal_order, normalOrder_normalOrder_left, normalOrder_normalOrder, normalOrder_superCommute_right_eq_zero, normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, normalOrder_uncontracted_none, normalOrder_anPart_mul_crPart, normalOrder_superCommute_eq_zero, ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum, normalOrder_ofFieldOpList_anPart_swap, normalOrder_uncontracted_some, normalOrder_ofCrAnOp_ofCrAnList, normalOrder_ofCrAnList, normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive, timeOrder_ofFieldOpList_eq_eqTimeOnly_empty, normalOrder_timeContract, normalOrder_anPart_ofFieldOpList_swap, normalOrder_mul_anPart, normalOrder_ofFieldOpList_mul_anPart_swap, WickContraction.staticWickTerm_insert_zero_none, normalOrder_ofFieldOp_ofFieldOp_swap, normalOrder_normalOrder_mid, normalOrder_superCommute_mid_eq_zero, crPart_mul_normalOrder, ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum, normalOrder_one_eq_one, timeOrder_haveEqTime_split, timeOrder_ofFieldOpList_eqTimeOnly
«term𝓝(_)» 📖» "API Documentation")	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ι_normalOrderF_eq_of_equiv 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra instSetoidFieldOpFreeAlgebra	FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF	—	ι_normalOrderF_zero_of_mem_ideal equiv_iff_sub_mem_ideal
ι_normalOrderF_superCommuteF_eq_zero 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	ι_normalOrderF_superCommuteF_eq_zero_mul
ι_normalOrderF_superCommuteF_eq_zero_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	FieldSpecification.FieldOpFreeAlgebra.ofListBasis_eq_ofList ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul
ι_normalOrderF_superCommuteF_eq_zero_mul_left 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	ι_normalOrderF_superCommuteF_eq_zero_mul
ι_normalOrderF_superCommuteF_eq_zero_mul_mul_right 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	ι_normalOrderF_superCommuteF_eq_zero_mul
ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	FieldSpecification.FieldOpFreeAlgebra.ofListBasis_eq_ofList ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero
ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF	—	FieldSpecification.FieldOpFreeAlgebra.ofListBasis_eq_ofList ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul
ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	CreateAnnihilate.eq_create_or_annihilate FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_ofCrAnListF_create_create_ofCrAnListF ι_superCommuteF_of_create_create FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_create_annihilate FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_annihilate_create FieldSpecification.FieldOpFreeAlgebra.normalOrderF_superCommuteF_ofCrAnListF_annihilate_annihilate_ofCrAnListF ι_superCommuteF_of_annihilate_annihilate
ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnListF_eq_zero_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF	—	FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul
ι_normalOrderF_superCommuteF_ofCrAnListF_ofCrAnOpF_eq_zero_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_singleton FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_symm FieldStatistic.ofList_singleton ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul
ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF	—	FieldSpecification.FieldOpFreeAlgebra.ofListBasis_eq_ofList ι_normalOrderF_superCommuteF_ofCrAnListF_eq_zero
ι_normalOrderF_superCommuteF_ofCrAnOpF_ofCrAnListF_eq_zero_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF	—	FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_singleton FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum ι_normalOrderF_superCommuteF_ofCrAnOpF_eq_zero_mul
ι_normalOrderF_zero_of_mem_ideal 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet	FieldSpecification.WickAlgebra ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF	—	ι_normalOrderF_superCommuteF_eq_zero_mul
ι_normalOrder_superCommuteF_eq_zero_mul_right 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.WickAlgebra FieldSpecification.CrAnFieldOp FieldSpecification.fieldOpIdealSet ι FieldSpecification.FieldOpFreeAlgebra.normalOrderF FieldSpecification.FieldOpFreeAlgebra.superCommuteF	—	ι_normalOrderF_superCommuteF_eq_zero_mul

---

← Back to Index