Perm

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/Perm.lean

Statistics

Metric	Count
Definitions Perm	1
Theorems isFull_of_isFull, perm_uncontractedList, refl, symm, trans	5
Total	6
⚠️ With sorry isFull_of_isFull, perm_uncontractedList	2

WickContraction

Definitions

Name	Category	Theorems
Perm 📖	MathDef	1 math math: Perm.refl

WickContraction.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isFull_of_isFull 📖 ⚠️	—	WickContraction.Perm WickContraction.IsFull FieldSpecification.FieldOp	—	—	—
perm_uncontractedList 📖 ⚠️	mathematical	WickContraction.Perm	FieldSpecification.FieldOp WickContraction.uncontractedListGet	—	—
refl 📖	mathematical	—	WickContraction.Perm	—	eq_1
symm 📖	—	WickContraction.Perm	—	—	eq_1
trans 📖	—	WickContraction.Perm	—	—	eq_1

---

← Back to Index