Documentation Verification Report

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	3 math math: `Perm.refl`, `Perm.trans`, `Perm.symm`

WickContraction.Perm

Theorems

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

---

← Back to Index