Documentation Verification Report

KoszulSignInsert

📁 Source: PhysLean/QFT/PerturbationTheory/Koszul/KoszulSignInsert.lean

Statistics

Metric	Count
Definitions `koszulSignCons`, `koszulSignInsert`	2
Theorems `koszulSignCons_eq_exchangeSign`, `koszulSignInsert_boson`, `koszulSignInsert_cons`, `koszulSignInsert_eq_cons`, `koszulSignInsert_eq_exchangeSign_take`, `koszulSignInsert_eq_filter`, `koszulSignInsert_eq_grade`, `koszulSignInsert_eq_perm`, `koszulSignInsert_eq_rel_eq_stat`, `koszulSignInsert_eq_remove_same_stat_append`, `koszulSignInsert_eq_sort`, `koszulSignInsert_ge_forall_append`, `koszulSignInsert_insertIdx`, `koszulSignInsert_le_forall`, `koszulSignInsert_mul_self`, `koszulSignInsert_of_le_mem`	16
Total	18

Wick

Definitions

Name	Category	Theorems
`koszulSignCons` 📖	CompOp	2 math math: `koszulSignInsert_cons`, `koszulSignCons_eq_exchangeSign`
`koszulSignInsert` 📖	CompOp	21 math math: `koszulSignInsert_eq_perm`, `koszulSignInsert_eq_exchangeSign_take`, `koszulSignInsert_insertIdx`, `koszulSignInsert_boson`, `koszulSignInsert_eq_grade`, `FieldSpecification.koszulSignInsert_create`, `koszulSignInsert_of_le_mem`, `koszulSignInsert_ge_forall_append`, `FieldSpecification.koszulSignInsert_swap`, `koszulSignInsert_mul_self`, `FieldSpecification.koszulSignInsert_crAnTimeOrderRel_crAnSection`, `koszulSignInsert_eq_rel_eq_stat`, `koszulSignInsert_erase_boson`, `koszulSignInsert_eq_remove_same_stat_append`, `FieldSpecification.koszulSignInsert_annihilate_cons_create`, `koszulSignInsert_eq_filter`, `koszulSignInsert_le_forall`, `koszulSignInsert_cons`, `FieldSpecification.koszulSignInsert_append_annihilate`, `koszulSignInsert_eq_sort`, `koszulSignInsert_eq_cons`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`koszulSignCons_eq_exchangeSign` 📖	mathematical	—	`koszulSignCons` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign`	—	`FieldStatistic.neq_fermionic_iff_eq_bosonic` `FieldStatistic.exchangeSign_bosonic` `FieldStatistic.bosonic_exchangeSign`
`koszulSignInsert_boson` 📖	mathematical	`FieldStatistic.bosonic`	`koszulSignInsert`	—	—
`koszulSignInsert_cons` 📖	mathematical	—	`koszulSignInsert` `koszulSignCons`	—	—
`koszulSignInsert_eq_cons` 📖	mathematical	—	`koszulSignInsert`	—	—
`koszulSignInsert_eq_exchangeSign_take` 📖	mathematical	—	`koszulSignInsert` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofList` `PhysLean.List.orderedInsertPos`	—	`koszulSignInsert_eq_cons` `koszulSignInsert_eq_sort` `koszulSignInsert_eq_filter` `koszulSignInsert_eq_grade` `FieldStatistic.exchangeSign_eq_if` `FieldStatistic.ofList_singleton` `PhysLean.List.orderedInsertPos_take`
`koszulSignInsert_eq_filter` 📖	mathematical	—	`koszulSignInsert`	—	`koszulSignInsert.congr_simp`
`koszulSignInsert_eq_grade` 📖	mathematical	—	`koszulSignInsert` `FieldStatistic` `FieldStatistic.ofList` `FieldStatistic.fermionic` `instDecidableEqFieldStatistic`	—	`FieldStatistic.ofList_singleton` `koszulSignInsert_eq_filter` `koszulSignInsert.congr_simp`
`koszulSignInsert_eq_perm` 📖	mathematical	—	`koszulSignInsert`	—	`koszulSignInsert_eq_grade` `FieldStatistic.ofList_perm`
`koszulSignInsert_eq_rel_eq_stat` 📖	mathematical	—	`koszulSignInsert`	—	—
`koszulSignInsert_eq_remove_same_stat_append` 📖	mathematical	—	`koszulSignInsert`	—	—
`koszulSignInsert_eq_sort` 📖	mathematical	—	`koszulSignInsert`	—	`koszulSignInsert_eq_perm`
`koszulSignInsert_ge_forall_append` 📖	mathematical	—	`koszulSignInsert`	—	—
`koszulSignInsert_insertIdx` 📖	mathematical	—	`koszulSignInsert`	—	`koszulSignInsert_eq_perm`
`koszulSignInsert_le_forall` 📖	mathematical	—	`koszulSignInsert`	—	—
`koszulSignInsert_mul_self` 📖	mathematical	—	`koszulSignInsert`	—	—
`koszulSignInsert_of_le_mem` 📖	mathematical	—	`koszulSignInsert`	—	—

---

← Back to Index