Documentation Verification Report

KoszulSign

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

Statistics

Metric	Count
Definitions `koszulSign`	1
Theorems `insertIdx_eraseIdx`, `koszulSignInsert_erase_boson`, `koszulSign_eq_rel_eq_stat`, `koszulSign_eq_rel_eq_stat_append`, `koszulSign_eraseIdx`, `koszulSign_eraseIdx_insertionSortMinPos`, `koszulSign_erase_boson`, `koszulSign_freeMonoid_of`, `koszulSign_insertIdx`, `koszulSign_mul_self`, `koszulSign_of_append_eq_insertionSort`, `koszulSign_of_append_eq_insertionSort_left`, `koszulSign_of_insertionSort`, `koszulSign_of_sorted`, `koszulSign_perm_eq`, `koszulSign_perm_eq_append`, `koszulSign_singleton`, `koszulSign_swap_eq_rel`, `koszulSign_swap_eq_rel_cons`	19
Total	20

Wick

Definitions

Name	Category	Theorems
`koszulSign` 📖	CompOp	17 math math: `koszulSign_eraseIdx_insertionSortMinPos`, `koszulSign_eq_rel_eq_stat`, `koszulSign_of_insertionSort`, `koszulSign_freeMonoid_of`, `koszulSign_of_append_eq_insertionSort_left`, `koszulSign_of_sorted`, `koszulSign_swap_eq_rel`, `koszulSign_singleton`, `koszulSign_of_append_eq_insertionSort`, `koszulSign_perm_eq_append`, `koszulSign_swap_eq_rel_cons`, `koszulSign_erase_boson`, `koszulSign_eraseIdx`, `koszulSign_mul_self`, `koszulSign_perm_eq`, `koszulSign_insertIdx`, `koszulSign_eq_rel_eq_stat_append`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`insertIdx_eraseIdx` 📖	—	—	—	—	—
`koszulSignInsert_erase_boson` 📖	mathematical	`FieldStatistic.bosonic`	`koszulSignInsert`	—	`koszulSignInsert.congr_simp` `koszulSignInsert.eq_2`
`koszulSign_eq_rel_eq_stat` 📖	mathematical	—	`koszulSign`	—	`koszulSign_eq_rel_eq_stat_append` `koszulSignInsert_eq_perm` `koszulSignInsert_eq_remove_same_stat_append`
`koszulSign_eq_rel_eq_stat_append` 📖	mathematical	—	`koszulSign`	—	`koszulSignInsert_eq_rel_eq_stat` `koszulSignInsert_mul_self`
`koszulSign_eraseIdx` 📖	mathematical	—	`koszulSign` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofList` `PhysLean.List.insertionSortEquiv`	—	`insertIdx_eraseIdx` `koszulSign_insertIdx` `PhysLean.List.insertionSortEquiv_congr` `FieldStatistic.exchangeSign_mul_self` `FieldStatistic.ofList_take_eraseIdx`
`koszulSign_eraseIdx_insertionSortMinPos` 📖	mathematical	—	`koszulSign` `PhysLean.List.insertionSortMinPos` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `PhysLean.List.insertionSortMin` `FieldStatistic.ofList`	—	`koszulSign_eraseIdx` `FieldStatistic.exchangeSign_bosonic`
`koszulSign_erase_boson` 📖	mathematical	`FieldStatistic.bosonic`	`koszulSign`	—	`koszulSign.congr_simp` `koszulSignInsert_boson` `koszulSign.eq_2` `koszulSignInsert_erase_boson`
`koszulSign_freeMonoid_of` 📖	mathematical	—	`koszulSign`	—	—
`koszulSign_insertIdx` 📖	mathematical	—	`koszulSign` `FieldStatistic` `FieldStatistic.instCommGroup` `FieldStatistic.exchangeSign` `FieldStatistic.ofList` `PhysLean.List.insertionSortEquiv`	—	`koszulSign_singleton` `FieldStatistic.exchangeSign_bosonic` `koszulSign.eq_2` `PhysLean.List.orderedInsertPos_lt_length` `PhysLean.Fin.equivCons_trans` `PhysLean.Fin.equivCons_zero` `PhysLean.List.orderedInsert_eq_insertIdx_orderedInsertPos` `FieldStatistic.ofList_take_insert` `koszulSignInsert_eq_exchangeSign_take` `FieldStatistic.ofList_take_zero` `PhysLean.Fin.equivCons_succ` `PhysLean.List.orderedInsertEquiv_fin_succ` `FieldStatistic.ofList_take_succ_cons` `koszulSignInsert_insertIdx` `koszulSignInsert_cons` `PhysLean.List.insertionSortEquiv_get` `PhysLean.List.lt_orderedInsertPos_rel` `PhysLean.List.gt_orderedInsertPos_rel` `FieldStatistic.ofList_take_insertIdx_gt` `koszulSignCons_eq_exchangeSign` `FieldStatistic.exchangeSign_symm` `FieldStatistic.ofList_take_insertIdx_le` `FieldStatistic.exchangeSign_mul_self` `koszulSignCons.eq_1`
`koszulSign_mul_self` 📖	mathematical	—	`koszulSign`	—	`koszulSignInsert_mul_self`
`koszulSign_of_append_eq_insertionSort` 📖	mathematical	—	`koszulSign`	—	`koszulSign_of_append_eq_insertionSort_left` `koszulSignInsert_eq_perm`
`koszulSign_of_append_eq_insertionSort_left` 📖	mathematical	—	`koszulSign`	—	`koszulSign.congr_simp` `koszulSign_of_insertionSort` `PhysLean.List.insertIdx_length_fst_append` `koszulSign_insertIdx` `FieldStatistic.ofList_insertionSort` `PhysLean.List.insertionSortEquiv_congr` `PhysLean.List.insertionSortEquiv_insertionSort_append` `PhysLean.List.insertionSort_insertionSort_append`
`koszulSign_of_insertionSort` 📖	mathematical	—	`koszulSign`	—	`koszulSign_of_sorted`
`koszulSign_of_sorted` 📖	mathematical	—	`koszulSign`	—	`koszulSignInsert_of_le_mem`
`koszulSign_perm_eq` 📖	mathematical	—	`koszulSign`	—	`koszulSign_perm_eq_append` `koszulSignInsert_eq_perm`
`koszulSign_perm_eq_append` 📖	mathematical	—	`koszulSign`	—	`koszulSignInsert_eq_perm` `koszulSign_swap_eq_rel_cons`
`koszulSign_singleton` 📖	mathematical	—	`koszulSign`	—	—
`koszulSign_swap_eq_rel` 📖	mathematical	—	`koszulSign`	—	`koszulSign_swap_eq_rel_cons` `koszulSignInsert_eq_perm`
`koszulSign_swap_eq_rel_cons` 📖	mathematical	—	`koszulSign`	—	—

---

← Back to Index