Documentation Verification Report

InsertNone

📁 Source: PhysLean/QFT/PerturbationTheory/WickContraction/Sign/InsertNone.lean

Statistics

Metric	Count
Definitions `signInsertNone`	1
Theorems `signFinset_insertAndContract_none`, `signInsertNone_eq_filter_map`, `signInsertNone_eq_filterset`, `signInsertNone_eq_mul_fst_snd`, `signInsertNone_eq_prod_getDual?_Some`, `signInsertNone_eq_prod_prod`, `sign_insert_none`, `sign_insert_none_eq_signInsertNone_mul_sign`, `sign_insert_none_zero`	9
Total	10

WickContraction

Definitions

Name	Category	Theorems
`signInsertNone` 📖	CompOp	6 math math: `sign_insert_none_eq_signInsertNone_mul_sign`, `signInsertNone_eq_filter_map`, `signInsertNone_eq_prod_getDual?_Some`, `signInsertNone_eq_prod_prod`, `signInsertNone_eq_filterset`, `signInsertNone_eq_mul_fst_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`signFinset_insertAndContract_none` 📖	mathematical	—	`signFinset` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted` `PhysLean.List.insertIdx_length_fin` `insertAndContractLiftFinset`	—	`PhysLean.List.insertIdx_length_fin` `insert_fin_eq_self` `insertAndContract_none_getDual?_self` `succAbove_mem_insertAndContractLiftFinset` `insertAndContract_none_getDual?_get_eq`
`signInsertNone_eq_filter_map` 📖	mathematical	`GradingCompliant`	`signInsertNone` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofList` `FieldSpecification.FieldOp` `getDual?`	—	`signInsertNone_eq_prod_getDual?_Some` `FieldStatistic.ofList_map_eq_finset_prod`
`signInsertNone_eq_filterset` 📖	mathematical	`GradingCompliant`	`signInsertNone` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `FieldSpecification.FieldOp` `getDual?`	—	`FieldStatistic.ofFinset_eq_prod` `signInsertNone_eq_prod_getDual?_Some`
`signInsertNone_eq_mul_fst_snd` 📖	mathematical	—	`signInsertNone` `FieldSpecification.FieldOp` `fstFieldOfContract` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `sndFieldOfContract`	—	`signInsertNone.eq_1` `fstFieldOfContract_lt_sndFieldOfContract` `FieldStatistic.exchangeSign_mul_self`
`signInsertNone_eq_prod_getDual?_Some` 📖	mathematical	`GradingCompliant`	`signInsertNone` `FieldSpecification.FieldOp` `getDual?` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic`	—	`signInsertNone_eq_prod_prod`
`signInsertNone_eq_prod_prod` 📖	mathematical	`GradingCompliant`	`signInsertNone` `FieldSpecification.FieldOp` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic`	—	`signInsertNone_eq_mul_fst_snd` `fstFieldOfContract_mem` `sndFieldOfContract_mem` `prod_finset_eq_mul_fst_snd`
`sign_insert_none` 📖	mathematical	`GradingCompliant`	`sign` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldSpecification.fieldOpStatistic` `FieldStatistic.ofFinset` `getDual?`	—	`sign_insert_none_eq_signInsertNone_mul_sign` `signInsertNone_eq_filterset`
`sign_insert_none_eq_signInsertNone_mul_sign` 📖	mathematical	—	`sign` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted` `signInsertNone`	—	`sign.eq_1` `signInsertNone.eq_1` `PhysLean.List.insertIdx_length_fin` `insertAndContract_none_prod_contractions` `insertAndContract_sndFieldOfContract` `PhysLean.List.insertIdx_getElem_fin` `insertAndContract_fstFieldOfContract` `signFinset_insertAndContract_none` `stat_ofFinset_of_insertAndContractLiftFinset` `FieldStatistic.ofFinset_insert` `FieldStatistic.exchangeSign_symm`
`sign_insert_none_zero` 📖	mathematical	—	`sign` `FieldSpecification.FieldOp` `insertAndContract` `uncontracted`	—	`sign_insert_none_eq_signInsertNone_mul_sign`

---

← Back to Index