Documentation Verification Report

OfFinset

📁 Source: PhysLean/QFT/PerturbationTheory/FieldStatistics/OfFinset.lean

Statistics

Metric	Count
Definitions `ofFinset`	1
Theorems `ofFinset_empty`, `ofFinset_eq_prod`, `ofFinset_erase`, `ofFinset_filter`, `ofFinset_filter_mul_neg`, `ofFinset_finset_map`, `ofFinset_insert`, `ofFinset_singleton`, `ofFinset_union`, `ofFinset_union_disjoint`	10
Total	11

FieldStatistic

Definitions

Name	Category	Theorems
`ofFinset` 📖	CompOp	40 math math: `WickContraction.wickTerm_insert_some`, `WickContraction.staticContract_insert_some_of_lt`, `WickContraction.sign_right_eq_prod_mul_prod`, `WickContraction.join_singleton_sign_right`, `FieldSpecification.FieldOpFreeAlgebra.timeOrderF_eq_maxTimeField_mul_finset`, `ofFinset_empty`, `WickContraction.wickTerm_insert_none`, `WickContraction.signInsertSomeCoef_eq_finset`, `WickContraction.stat_signFinset_right`, `ofFinset_union_disjoint`, `ofFinset_union`, `WickContraction.signInsertSome_mul_filter_contracted_of_lt`, `ofFinset_eq_prod`, `WickContraction.signInsertSomeProd_eq_finset`, `WickContraction.sign_insert_some_of_not_lt`, `FieldSpecification.WickAlgebra.timeOrder_eq_maxTimeField_mul_finset`, `ofFinset_erase`, `WickContraction.timeContract_insert_some_of_not_lt`, `ofFinset_insert`, `WickContraction.join_singleton_sign_left`, `WickContraction.signInsertSomeCoef_if`, `WickContraction.sign_insert_some_zero`, `WickContraction.timeContract_insert_some_of_lt`, `WickContraction.joinSignRightExtra_eq_i_j_finset_eq_if`, `WickContraction.signInsertSome_mul_filter_contracted_of_not_lt`, `WickContraction.stat_ofFinset_of_insertAndContractLiftFinset`, `WickContraction.mul_wickTerm_eq_sum`, `ofFinset_singleton`, `FieldSpecification.WickAlgebra.normalOrder_uncontracted_none`, `ofFinset_filter`, `WickContraction.stat_ofFinset_eq_one_of_gradingCompliant`, `WickContraction.stat_signFinset_insert_some_self_fst`, `WickContraction.singleton_sign_expand`, `WickContraction.join_singleton_left_signFinset_eq_filter`, `ofFinset_finset_map`, `WickContraction.signInsertNone_eq_filterset`, `WickContraction.stat_signFinset_insert_some_self_snd`, `WickContraction.sign_insert_some_of_lt`, `WickContraction.sign_insert_none`, `ofFinset_filter_mul_neg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofFinset_empty` 📖	mathematical	—	`ofFinset` `FieldStatistic` `instCommGroup`	—	—
`ofFinset_eq_prod` 📖	mathematical	—	`ofFinset` `FieldStatistic` `instCommGroup`	—	`ofFinset.eq_1` `ofList_map_eq_finset_prod`
`ofFinset_erase` 📖	mathematical	—	`ofFinset` `FieldStatistic` `instCommGroup`	—	`ofFinset_insert` `mul_self`
`ofFinset_filter` 📖	mathematical	—	`ofFinset` `FieldStatistic` `instCommGroup`	—	`ofFinset_filter_mul_neg` `mul_self`
`ofFinset_filter_mul_neg` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `ofFinset`	—	`ofFinset_union_disjoint`
`ofFinset_finset_map` 📖	mathematical	—	`ofFinset`	—	`ofList_perm`
`ofFinset_insert` 📖	mathematical	—	`ofFinset` `FieldStatistic` `instCommGroup`	—	`ofList_cons_eq_mul` `ofList_perm`
`ofFinset_singleton` 📖	mathematical	—	`ofFinset`	—	`ofList_singleton`
`ofFinset_union` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `ofFinset`	—	`ofFinset_eq_prod` `mul_self`
`ofFinset_union_disjoint` 📖	mathematical	—	`FieldStatistic` `instCommGroup` `ofFinset`	—	`ofFinset_union`

---

← Back to Index