Documentation Verification Report

CrAnSection

📁 Source: PhysLean/QFT/PerturbationTheory/FieldSpecification/CrAnSection.lean

Statistics

MetricCount
DefinitionsCrAnSection, append, appendEquiv, congr, cons, consEquiv, drop, eraseIdx, eraseIdxEquiv, fintype, head, nilEquiv, singletonEquiv, tail, take
15
Theoremsappend_assoc, append_assoc', card_cons_eq, card_eq_mul, card_nil_eq, card_perm_eq, congr_append, congr_fst, congr_fst_append, congr_snd_append, congr_symm, congr_trans_apply, drop_congr, drop_left, eq_head_cons_tail, eraseIdxEquiv_apply_snd, eraseIdxEquiv_symm_eq_take_cons_drop, eraseIdxEquiv_symm_eraseIdx, eraseIdxEquiv_symm_getElem, head_state_eq, length_eq, singletonEquiv_append_eq_cons, statistics_eq_state_statistics, sum_cons, sum_eraseIdxEquiv, sum_nil, sum_over_length, take_append_drop, take_congr, take_left, take_statistics_eq_take_state_statistics, map_eraseIdx
32
Total47

FieldSpecification

Definitions

NameCategoryTheorems
CrAnSection 📖CompOp
30 mathmath: CrAnSection.congr_trans_apply, CrAnSection.take_congr, CrAnSection.drop_left, CrAnSection.congr_snd_append, CrAnSection.congr_fst, CrAnSection.congr_symm, WickAlgebra.ofFieldOpList_eq_sum, CrAnSection.sum_eraseIdxEquiv, CrAnSection.eraseIdxEquiv_apply_snd, CrAnSection.append_assoc, CrAnSection.singletonEquiv_append_eq_cons, CrAnSection.take_append_drop, sum_crAnSections_timeOrder, FieldOpFreeAlgebra.ofFieldOpListF_sum, CrAnSection.eraseIdxEquiv_symm_eq_take_cons_drop, CrAnSection.congr_append, CrAnSection.card_eq_mul, CrAnSection.eraseIdxEquiv_symm_eraseIdx, CrAnSection.card_cons_eq, CrAnSection.sum_nil, CrAnSection.append_assoc', CrAnSection.take_left, CrAnSection.drop_congr, crAnSectionTimeOrder_bijective, crAnSectionTimeOrder_injective, CrAnSection.card_nil_eq, CrAnSection.card_perm_eq, CrAnSection.eraseIdxEquiv_symm_getElem, CrAnSection.sum_cons, CrAnSection.congr_fst_append

FieldSpecification.CrAnSection

Definitions

NameCategoryTheorems
append 📖CompOp
10 mathmath: drop_left, congr_snd_append, append_assoc, singletonEquiv_append_eq_cons, take_append_drop, eraseIdxEquiv_symm_eq_take_cons_drop, congr_append, append_assoc', take_left, congr_fst_append
appendEquiv 📖CompOp—
congr 📖CompOp
14 mathmath: congr_trans_apply, take_congr, drop_left, congr_snd_append, congr_fst, congr_symm, append_assoc, take_append_drop, eraseIdxEquiv_symm_eq_take_cons_drop, congr_append, append_assoc', take_left, drop_congr, congr_fst_append
cons 📖CompOp
3 mathmath: singletonEquiv_append_eq_cons, eraseIdxEquiv_symm_eq_take_cons_drop, sum_cons
consEquiv 📖CompOp—
drop 📖CompOp
4 mathmath: drop_left, take_append_drop, eraseIdxEquiv_symm_eq_take_cons_drop, drop_congr
eraseIdx 📖CompOp
1 mathmath: eraseIdxEquiv_apply_snd
eraseIdxEquiv 📖CompOp
5 mathmath: sum_eraseIdxEquiv, eraseIdxEquiv_apply_snd, eraseIdxEquiv_symm_eq_take_cons_drop, eraseIdxEquiv_symm_eraseIdx, eraseIdxEquiv_symm_getElem
fintype 📖CompOp
10 mathmath: FieldSpecification.WickAlgebra.ofFieldOpList_eq_sum, sum_eraseIdxEquiv, FieldSpecification.sum_crAnSections_timeOrder, FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF_sum, card_eq_mul, card_cons_eq, sum_nil, card_nil_eq, card_perm_eq, sum_cons
head 📖CompOp
1 mathmath: eq_head_cons_tail
nilEquiv 📖CompOp—
singletonEquiv 📖CompOp
1 mathmath: singletonEquiv_append_eq_cons
tail 📖CompOp
1 mathmath: eq_head_cons_tail
take 📖CompOp
4 mathmath: take_congr, take_append_drop, eraseIdxEquiv_symm_eq_take_cons_drop, take_left

Theorems

NameKindAssumesProvesValidatesDepends On
append_assoc 📖mathematical—append
FieldSpecification.FieldOp
FieldSpecification.CrAnSection
congr		—congr_fst
append_assoc' 📖mathematical—append
FieldSpecification.FieldOp
FieldSpecification.CrAnSection
congr		—congr_fst
card_cons_eq 📖mathematical—FieldSpecification.CrAnSection
FieldSpecification.FieldOp
fintype
FieldSpecification.fieldOpToCrAnType
FieldSpecification.instFintypeFieldOpToCrAnType		——
card_eq_mul 📖mathematical—FieldSpecification.CrAnSection
fintype
FieldSpecification.FieldOp
FieldSpecification.statesIsPosition		—card_nil_eq
card_cons_eq
card_nil_eq 📖mathematical—FieldSpecification.CrAnSection
FieldSpecification.FieldOp
fintype		——
card_perm_eq 📖mathematicalFieldSpecification.FieldOpFieldSpecification.CrAnSection
fintype		—card_eq_mul
congr_append 📖mathematical—append
FieldSpecification.CrAnSection
congr
FieldSpecification.FieldOp		——
congr_fst 📖mathematical—FieldSpecification.CrAnFieldOp
FieldSpecification.FieldOp
FieldSpecification.crAnFieldOpToFieldOp
FieldSpecification.CrAnSection
congr		——
congr_fst_append 📖mathematical—append
FieldSpecification.CrAnSection
congr
FieldSpecification.FieldOp		——
congr_snd_append 📖mathematical—append
FieldSpecification.CrAnSection
congr
FieldSpecification.FieldOp		——
congr_symm 📖mathematical—FieldSpecification.CrAnSection
congr
FieldSpecification.FieldOp		——
congr_trans_apply 📖mathematical—FieldSpecification.CrAnSection
congr
FieldSpecification.FieldOp		——
drop_congr 📖mathematical—drop
FieldSpecification.CrAnSection
congr
FieldSpecification.FieldOp		——
drop_left 📖mathematical—drop
FieldSpecification.FieldOp
append
FieldSpecification.CrAnSection
congr		—length_eq
congr_fst
eq_head_cons_tail 📖mathematical—FieldSpecification.CrAnFieldOp
FieldSpecification.FieldOp
FieldSpecification.crAnFieldOpToFieldOp
FieldSpecification.fieldOpToCrAnType
head
tail		—length_eq
head_state_eq
eraseIdxEquiv_apply_snd 📖mathematicalFieldSpecification.FieldOpFieldSpecification.fieldOpToCrAnType
FieldSpecification.CrAnSection
eraseIdxEquiv
eraseIdx		—congr_fst
eraseIdxEquiv_symm_eq_take_cons_drop 📖mathematicalFieldSpecification.FieldOpFieldSpecification.fieldOpToCrAnType
FieldSpecification.CrAnSection
eraseIdxEquiv
congr
PhysLean.List.take_eraseIdx_same
PhysLean.List.drop_eraseIdx_succ
append
take
cons
drop		—PhysLean.List.take_eraseIdx_same
PhysLean.List.drop_eraseIdx_succ
congr_symm
take_congr
congr_trans_apply
drop_congr
congr_fst_append
congr_snd_append
append_assoc'
singletonEquiv_append_eq_cons
congr_fst
eraseIdxEquiv_symm_eraseIdx 📖mathematicalFieldSpecification.FieldOpFieldSpecification.CrAnFieldOp
FieldSpecification.crAnFieldOpToFieldOp
FieldSpecification.fieldOpToCrAnType
FieldSpecification.CrAnSection
eraseIdxEquiv		—eraseIdxEquiv_apply_snd
eraseIdxEquiv_symm_getElem 📖mathematicalFieldSpecification.FieldOpFieldSpecification.CrAnFieldOp
FieldSpecification.crAnFieldOpToFieldOp
FieldSpecification.fieldOpToCrAnType
FieldSpecification.CrAnSection
eraseIdxEquiv
length_eq		—length_eq
PhysLean.List.take_eraseIdx_same
PhysLean.List.drop_eraseIdx_succ
eraseIdxEquiv_symm_eq_take_cons_drop
congr_fst
PhysLean.List.eraseIdx_length
head_state_eq 📖mathematical—FieldSpecification.FieldOp
FieldSpecification.fieldOpToCrAnType
FieldSpecification.CrAnFieldOp
FieldSpecification.crAnFieldOpToFieldOp
length_eq		—length_eq
length_eq 📖mathematical—FieldSpecification.CrAnFieldOp
FieldSpecification.FieldOp
FieldSpecification.crAnFieldOpToFieldOp		——
singletonEquiv_append_eq_cons 📖mathematical—append
FieldSpecification.FieldOp
FieldSpecification.fieldOpToCrAnType
FieldSpecification.CrAnSection
singletonEquiv
cons		——
statistics_eq_state_statistics 📖mathematical—FieldStatistic.ofList
FieldSpecification.CrAnFieldOp
FieldSpecification.crAnStatistics
FieldSpecification.FieldOp
FieldSpecification.crAnFieldOpToFieldOp
FieldSpecification.fieldOpStatistic		—FieldStatistic.ofList_eq_prod
FieldSpecification.crAnStatistics.eq_1
sum_cons 📖mathematical—FieldSpecification.CrAnSection
FieldSpecification.FieldOp
fintype
FieldSpecification.fieldOpToCrAnType
FieldSpecification.instFintypeFieldOpToCrAnType
cons		——
sum_eraseIdxEquiv 📖mathematicalFieldSpecification.FieldOpFieldSpecification.CrAnSection
fintype
FieldSpecification.fieldOpToCrAnType
FieldSpecification.instFintypeFieldOpToCrAnType
eraseIdxEquiv		——
sum_nil 📖mathematical—FieldSpecification.CrAnSection
FieldSpecification.FieldOp
fintype
FieldSpecification.CrAnFieldOp
FieldSpecification.crAnFieldOpToFieldOp		——
sum_over_length 📖mathematical—FieldSpecification.CrAnFieldOp
FieldSpecification.FieldOp
FieldSpecification.crAnFieldOpToFieldOp
length_eq		—length_eq
take_append_drop 📖mathematical—append
FieldSpecification.FieldOp
take
drop
FieldSpecification.CrAnSection
congr		—congr_fst
take_congr 📖mathematical—take
FieldSpecification.CrAnSection
congr
FieldSpecification.FieldOp		——
take_left 📖mathematical—take
FieldSpecification.FieldOp
append
FieldSpecification.CrAnSection
congr		—length_eq
congr_fst
take_statistics_eq_take_state_statistics 📖mathematical—FieldStatistic.ofList
FieldSpecification.CrAnFieldOp
FieldSpecification.crAnStatistics
FieldSpecification.FieldOp
FieldSpecification.crAnFieldOpToFieldOp
FieldSpecification.fieldOpStatistic		—FieldStatistic.ofList_eq_prod
FieldSpecification.crAnStatistics.eq_1

List

Theorems

NameKindAssumesProvesValidatesDepends On
map_eraseIdx 📖—————

---

← Back to Index