IsFull

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

Statistics

Metric	Count
Definitions IsFull, instDecidableIsFull, isFullInvolutionEquiv	3
Theorems card_of_isfull_even, card_of_isfull_odd, isFull_iff_equivInvolution_no_fixed_point	3
Total	6

WickContraction

Definitions

Name	Category	Theorems
IsFull 📖	MathDef	3 math math: card_of_isfull_even, card_of_isfull_odd, isFull_iff_equivInvolution_no_fixed_point
instDecidableIsFull 📖	CompOp	2 math math: card_of_isfull_even, card_of_isfull_odd
isFullInvolutionEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_of_isfull_even 📖	mathematical	—	WickContraction IsFull instDecidableIsFull fintype_succ	—	PhysLean.Fin.involutionNoFixed_card_even
card_of_isfull_odd 📖	mathematical	—	WickContraction IsFull instDecidableIsFull fintype_succ	—	PhysLean.Fin.involutionNoFixed_card_odd
isFull_iff_equivInvolution_no_fixed_point 📖	mathematical	—	IsFull	—	—

---

← Back to Index