Documentation Verification Report

Card

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

Statistics

Metric	Count
Definitions `cardFun`, `consAddContract`	2
Theorems `card_eq_cardFun`, `consAddContract_bijection`, `consAddContract_getDual?_self_succ`, `consAddContract_getDual?_zero`, `consAddContract_injective`, `consAddContract_surjective_on_zero_contract`, `finset_succAbove_succ_disjoint`, `mem_consAddContract_of_mem_iff`, `wickContraction_card_eq_sum_zero_none_isSome`, `wickContraction_zero_none_card`, `wickContraction_zero_some_eq_mul`, `wickContraction_zero_some_eq_sum`	12
Total	14

WickContraction

Definitions

Name	Category	Theorems
`cardFun` 📖	CompOp	1 math math: `card_eq_cardFun`
`consAddContract` 📖	CompOp	6 math math: `consAddContract_getDual?_zero`, `consAddContract_surjective_on_zero_contract`, `consAddContract_injective`, `consAddContract_getDual?_self_succ`, `mem_consAddContract_of_mem_iff`, `consAddContract_bijection`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_eq_cardFun` 📖	mathematical	—	`WickContraction` `fintype_succ` `cardFun`	—	`wickContraction_card_eq_sum_zero_none_isSome` `wickContraction_zero_none_card` `wickContraction_zero_some_eq_mul`
`consAddContract_bijection` 📖	mathematical	—	`WickContraction` `getDual?` `consAddContract` `consAddContract_getDual?_zero`	—	`consAddContract_getDual?_zero` `consAddContract_injective` `consAddContract_surjective_on_zero_contract`
`consAddContract_getDual?_self_succ` 📖	mathematical	—	`getDual?` `consAddContract`	—	`getDual?_eq_some_iff_mem`
`consAddContract_getDual?_zero` 📖	mathematical	—	`getDual?` `consAddContract`	—	`getDual?_eq_some_iff_mem`
`consAddContract_injective` 📖	mathematical	—	`WickContraction` `consAddContract`	—	`mem_consAddContract_of_mem_iff`
`consAddContract_surjective_on_zero_contract` 📖	mathematical	`getDual?`	`consAddContract`	—	—
`finset_succAbove_succ_disjoint` 📖	—	—	—	—	—
`mem_consAddContract_of_mem_iff` 📖	mathematical	—	`consAddContract`	—	`finset_succAbove_succ_disjoint`
`wickContraction_card_eq_sum_zero_none_isSome` 📖	mathematical	—	`WickContraction` `fintype_succ` `getDual?`	—	—
`wickContraction_zero_none_card` 📖	mathematical	—	`WickContraction` `getDual?` `fintype_succ`	—	`insertAndContractNat_none_getDual?_eq_none` `insertAndContractNat_bijective`
`wickContraction_zero_some_eq_mul` 📖	mathematical	—	`WickContraction` `getDual?` `fintype_succ`	—	`wickContraction_zero_some_eq_sum` `consAddContract_getDual?_zero` `consAddContract_bijection`
`wickContraction_zero_some_eq_sum` 📖	mathematical	—	`WickContraction` `getDual?` `fintype_succ`	—	—

---

← Back to Index