Documentation Verification Report

StaticWickTerm

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

Statistics

MetricCount
DefinitionsstaticWickTerm
1
Theoremsmul_staticWickTerm_eq_sum, staticWickTerm_empty_nil, staticWickTerm_insert_zero_none, staticWickTerm_insert_zero_some
4
Total5

WickContraction

Definitions

NameCategoryTheorems
staticWickTerm 📖CompOp
5 mathmath: staticWickTerm_insert_zero_some, mul_staticWickTerm_eq_sum, FieldSpecification.WickAlgebra.static_wick_theorem, staticWickTerm_empty_nil, staticWickTerm_insert_zero_none

Theorems

NameKindAssumesProvesValidatesDepends On
mul_staticWickTerm_eq_sum 📖mathematical—FieldSpecification.WickAlgebra
FieldSpecification.FieldOpFreeAlgebra
FieldSpecification.CrAnFieldOp
FieldSpecification.fieldOpIdealSet
FieldSpecification.WickAlgebra.ofFieldOp
staticWickTerm
FieldSpecification.FieldOp
uncontracted
insertAndContract		—FieldSpecification.WickAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum
uncontractedFieldOpEquiv_list_sum
staticWickTerm_insert_zero_none
staticWickTerm_insert_zero_some
staticWickTerm_empty_nil 📖mathematical—staticWickTerm
FieldSpecification.FieldOp
empty
FieldSpecification.WickAlgebra
FieldSpecification.FieldOpFreeAlgebra
FieldSpecification.CrAnFieldOp
FieldSpecification.fieldOpIdealSet		—staticWickTerm.eq_1
uncontractedListGet.eq_1
nil_zero_uncontractedList
FieldSpecification.WickAlgebra.normalOrder_ofFieldOpList_nil
staticWickTerm_insert_zero_none 📖mathematical—staticWickTerm
FieldSpecification.FieldOp
insertAndContract
uncontracted
FieldSpecification.WickAlgebra
FieldSpecification.FieldOpFreeAlgebra
FieldSpecification.CrAnFieldOp
FieldSpecification.fieldOpIdealSet
sign
staticContract
FieldSpecification.WickAlgebra.normalOrder
FieldSpecification.WickAlgebra.ofFieldOpList
uncontractedListGet		—staticWickTerm.eq_1
sign_insert_none_zero
staticContract_insert_none
insertAndContract_uncontractedList_none_zero
staticWickTerm_insert_zero_some 📖mathematical—staticWickTerm
FieldSpecification.FieldOp
insertAndContract
uncontracted
FieldSpecification.WickAlgebra
FieldSpecification.FieldOpFreeAlgebra
FieldSpecification.CrAnFieldOp
FieldSpecification.fieldOpIdealSet
sign
staticContract
FieldSpecification.WickAlgebra.contractStateAtIndex
uncontractedListGet
uncontractedFieldOpEquiv
FieldSpecification.WickAlgebra.normalOrder
FieldSpecification.WickAlgebra.ofFieldOpList
PhysLean.List.optionEraseZ		—staticWickTerm.eq_1
FieldSpecification.WickAlgebra.normalOrder_uncontracted_some
staticContract_insert_some_of_lt
sign_insert_some_zero
FieldStatistic.exchangeSign_mul_self
staticContract_of_not_gradingCompliant
uncontractedList_getElem_uncontractedIndexEquiv_symm
FieldSpecification.WickAlgebra.superCommute_anPart_ofFieldOpF_diff_grade_zero

---

← Back to Index