Grading

📁 Source: PhysLean/QFT/PerturbationTheory/WickAlgebra/Grading.lean

Statistics

Metric	Count
Definitions `WickAlgebraGrade`, `bosonicProj`, `bosonicProjFree`, `fermionicProj`, `fermionicProjFree`, `statSubmodule`, `ιStateSubmodule`	7
Theorems `bosonicProjFree_eq_of_equiv`, `bosonicProjFree_eq_ι_bosonicProjF`, `bosonicProjFree_zero_of_ι_zero`, `bosonicProj_add_fermionicProj`, `bosonicProj_bosonicProj_eq_bosonicProj`, `bosonicProj_eq_bosonicProjFree`, `bosonicProj_fermionicProj_eq_zero`, `bosonicProj_mem_bosonic`, `bosonicProj_mem_fermionic`, `bosonicProj_of_bosonic_part`, `bosonicProj_of_fermionic_part`, `coeAddMonoidHom_apply_eq_bosonic_plus_fermionic`, `directSum_eq_bosonic_plus_fermionic`, `eq_zero_of_bosonic_and_fermionic`, `fermionicProjFree_eq_of_equiv`, `fermionicProjFree_eq_ι_fermionicProjF`, `fermionicProjFree_zero_of_ι_zero`, `fermionicProj_bosonicProj_eq_zero`, `fermionicProj_eq_fermionicProjFree`, `fermionicProj_fermionicProj_eq_fermionicProj`, `fermionicProj_mem_bosonic`, `fermionicProj_mem_fermionic`, `fermionicProj_of_bosonic_part`, `fermionicProj_of_fermionic_part`, `mem_bosonic_iff_fermionicProj_eq_zero`, `mem_bosonic_of_mem_free_bosonic`, `mem_fermionic_iff_bosonicProj_eq_zero`, `mem_fermionic_of_mem_free_fermionic`, `mem_statSubmodule_of_mem_statisticSubmodule`, `ofCrAnList_mem_statSubmodule`, `ofCrAnList_mem_statSubmodule_of_eq`	31
Total	38

FieldSpecification.WickAlgebra

Definitions

Name	Category	Theorems
`WickAlgebraGrade` 📖	CompOp	—
`bosonicProj` 📖	CompOp	10 math math: `bosonicProj_fermionicProj_eq_zero`, `bosonicProj_of_bosonic_part`, `bosonicProj_add_fermionicProj`, `mem_fermionic_iff_bosonicProj_eq_zero`, `bosonicProj_mem_bosonic`, `bosonicProj_bosonicProj_eq_bosonicProj`, `bosonicProj_mem_fermionic`, `bosonicProj_eq_bosonicProjFree`, `bosonicProj_of_fermionic_part`, `fermionicProj_bosonicProj_eq_zero`
`bosonicProjFree` 📖	CompOp	4 math math: `bosonicProjFree_zero_of_ι_zero`, `bosonicProj_eq_bosonicProjFree`, `bosonicProjFree_eq_ι_bosonicProjF`, `bosonicProjFree_eq_of_equiv`
`fermionicProj` 📖	CompOp	10 math math: `fermionicProj_fermionicProj_eq_fermionicProj`, `bosonicProj_fermionicProj_eq_zero`, `bosonicProj_add_fermionicProj`, `fermionicProj_eq_fermionicProjFree`, `fermionicProj_mem_bosonic`, `fermionicProj_of_fermionic_part`, `mem_bosonic_iff_fermionicProj_eq_zero`, `fermionicProj_mem_fermionic`, `fermionicProj_of_bosonic_part`, `fermionicProj_bosonicProj_eq_zero`
`fermionicProjFree` 📖	CompOp	4 math math: `fermionicProjFree_eq_of_equiv`, `fermionicProjFree_eq_ι_fermionicProjF`, `fermionicProj_eq_fermionicProjFree`, `fermionicProjFree_zero_of_ι_zero`
`statSubmodule` 📖	CompOp	26 math math: `fermionicProjFree_eq_of_equiv`, `fermionicProj_fermionicProj_eq_fermionicProj`, `fermionicProjFree_eq_ι_fermionicProjF`, `bosonicProj_fermionicProj_eq_zero`, `bosonicProj_of_bosonic_part`, `bosonicProj_add_fermionicProj`, `mem_fermionic_iff_bosonicProj_eq_zero`, `mem_fermionic_of_mem_free_fermionic`, `mem_bosonic_of_mem_free_bosonic`, `bosonicProj_bosonicProj_eq_bosonicProj`, `bosonicProjFree_zero_of_ι_zero`, `fermionicProj_eq_fermionicProjFree`, `fermionicProj_of_fermionic_part`, `bosonicProj_eq_bosonicProjFree`, `mem_bosonic_iff_fermionicProj_eq_zero`, `bosonicProj_of_fermionic_part`, `fermionicProj_of_bosonic_part`, `ofCrAnList_mem_statSubmodule`, `mem_statSubmodule_of_mem_statisticSubmodule`, `bosonicProjFree_eq_ι_bosonicProjF`, `fermionicProj_bosonicProj_eq_zero`, `bosonicProjFree_eq_of_equiv`, `directSum_eq_bosonic_plus_fermionic`, `fermionicProjFree_zero_of_ι_zero`, `coeAddMonoidHom_apply_eq_bosonic_plus_fermionic`, `ofCrAnList_mem_statSubmodule_of_eq`
`ιStateSubmodule` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bosonicProjFree_eq_of_equiv` 📖	mathematical	`FieldSpecification.FieldOpFreeAlgebra` `instSetoidFieldOpFreeAlgebra`	`FieldSpecification.WickAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `bosonicProjFree`	—	`bosonicProjFree_zero_of_ι_zero` `ι_eq_zero_iff_mem_ideal` `equiv_iff_sub_mem_ideal`
`bosonicProjFree_eq_ι_bosonicProjF` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `bosonicProjFree` `ι` `FieldSpecification.FieldOpFreeAlgebra.statisticSubmodule` `FieldSpecification.FieldOpFreeAlgebra.bosonicProjF`	—	—
`bosonicProjFree_zero_of_ι_zero` 📖	mathematical	`FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.WickAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `ι`	`statSubmodule` `FieldStatistic.bosonic` `bosonicProjFree`	—	`bosonicProjFree_eq_ι_bosonicProjF` `ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero`
`bosonicProj_add_fermionicProj` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `bosonicProj` `FieldStatistic.fermionic` `fermionicProj`	—	`ι_surjective` `fermionicProj_eq_fermionicProjFree` `bosonicProj_eq_bosonicProjFree` `bosonicProjFree_eq_ι_bosonicProjF` `fermionicProjFree_eq_ι_fermionicProjF` `FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_add_fermionicProjF`
`bosonicProj_bosonicProj_eq_bosonicProj` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `bosonicProj`	—	`bosonicProj_mem_bosonic` `bosonicProjFree_eq_of_equiv`
`bosonicProj_eq_bosonicProjFree` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `bosonicProj` `ι` `bosonicProjFree`	—	—
`bosonicProj_fermionicProj_eq_zero` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `bosonicProj` `FieldStatistic.fermionic` `fermionicProj`	—	`bosonicProj_mem_fermionic`
`bosonicProj_mem_bosonic` 📖	mathematical	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic`	`bosonicProj`	—	`ofCrAnList.eq_1` `bosonicProj_eq_bosonicProjFree` `bosonicProjFree_eq_ι_bosonicProjF` `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mem_statisticSubmodule_of` `FieldSpecification.FieldOpFreeAlgebra.bosonicProjF_of_mem_bosonic`
`bosonicProj_mem_fermionic` 📖	mathematical	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic`	`FieldStatistic.bosonic` `bosonicProj`	—	`bosonicProj_add_fermionicProj` `fermionicProj_mem_fermionic`
`bosonicProj_of_bosonic_part` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `bosonicProj` `FieldStatistic`	—	`bosonicProj_mem_bosonic`
`bosonicProj_of_fermionic_part` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `bosonicProj` `FieldStatistic.fermionic` `FieldStatistic`	—	`bosonicProj_mem_fermionic`
`coeAddMonoidHom_apply_eq_bosonic_plus_fermionic` 📖	mathematical	—	`FieldStatistic` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `instDecidableEqFieldStatistic` `FieldStatistic.bosonic` `FieldStatistic.fermionic`	—	—
`directSum_eq_bosonic_plus_fermionic` 📖	mathematical	—	`FieldStatistic` `FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `instDecidableEqFieldStatistic` `FieldStatistic.fermionic`	—	—
`eq_zero_of_bosonic_and_fermionic` 📖	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `FieldStatistic.fermionic`	—	—	`bosonicProj_mem_bosonic` `fermionicProj_mem_fermionic` `bosonicProj_add_fermionicProj`
`fermionicProjFree_eq_of_equiv` 📖	mathematical	`FieldSpecification.FieldOpFreeAlgebra` `instSetoidFieldOpFreeAlgebra`	`FieldSpecification.WickAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic` `fermionicProjFree`	—	`fermionicProjFree_zero_of_ι_zero` `ι_eq_zero_iff_mem_ideal` `equiv_iff_sub_mem_ideal`
`fermionicProjFree_eq_ι_fermionicProjF` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic` `fermionicProjFree` `ι` `FieldSpecification.FieldOpFreeAlgebra.statisticSubmodule` `FieldSpecification.FieldOpFreeAlgebra.fermionicProjF`	—	—
`fermionicProjFree_zero_of_ι_zero` 📖	mathematical	`FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.WickAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `ι`	`statSubmodule` `FieldStatistic.fermionic` `fermionicProjFree`	—	`fermionicProjFree_eq_ι_fermionicProjF` `ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero`
`fermionicProj_bosonicProj_eq_zero` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic` `fermionicProj` `FieldStatistic.bosonic` `bosonicProj`	—	`fermionicProj_mem_bosonic`
`fermionicProj_eq_fermionicProjFree` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic` `fermionicProj` `ι` `fermionicProjFree`	—	—
`fermionicProj_fermionicProj_eq_fermionicProj` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic` `fermionicProj`	—	`fermionicProj_mem_fermionic` `fermionicProjFree_eq_of_equiv`
`fermionicProj_mem_bosonic` 📖	mathematical	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic`	`FieldStatistic.fermionic` `fermionicProj`	—	`bosonicProj_add_fermionicProj` `bosonicProj_mem_bosonic`
`fermionicProj_mem_fermionic` 📖	mathematical	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic`	`fermionicProj`	—	`ofCrAnList.eq_1` `fermionicProj_eq_fermionicProjFree` `fermionicProjFree_eq_ι_fermionicProjF` `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF_mem_statisticSubmodule_of` `FieldSpecification.FieldOpFreeAlgebra.fermionicProjF_of_mem_fermionic`
`fermionicProj_of_bosonic_part` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic` `fermionicProj` `FieldStatistic.bosonic` `FieldStatistic`	—	`fermionicProj_mem_bosonic`
`fermionicProj_of_fermionic_part` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic` `fermionicProj` `FieldStatistic`	—	`fermionicProj_mem_fermionic`
`mem_bosonic_iff_fermionicProj_eq_zero` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.bosonic` `FieldStatistic.fermionic` `fermionicProj`	—	`fermionicProj_mem_bosonic` `bosonicProj_add_fermionicProj`
`mem_bosonic_of_mem_free_bosonic` 📖	mathematical	`FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.FieldOpFreeAlgebra.statisticSubmodule` `FieldStatistic.bosonic`	`FieldSpecification.WickAlgebra` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `ι`	—	`ofCrAnList_mem_statSubmodule_of_eq`
`mem_fermionic_iff_bosonicProj_eq_zero` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.fermionic` `FieldStatistic.bosonic` `bosonicProj`	—	`bosonicProj_mem_fermionic` `bosonicProj_add_fermionicProj`
`mem_fermionic_of_mem_free_fermionic` 📖	mathematical	`FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.FieldOpFreeAlgebra.statisticSubmodule` `FieldStatistic.fermionic`	`FieldSpecification.WickAlgebra` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `ι`	—	`ofCrAnList_mem_statSubmodule_of_eq`
`mem_statSubmodule_of_mem_statisticSubmodule` 📖	mathematical	`FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.FieldOpFreeAlgebra.statisticSubmodule`	`FieldSpecification.WickAlgebra` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `ι`	—	`mem_bosonic_of_mem_free_bosonic` `mem_fermionic_of_mem_free_fermionic`
`ofCrAnList_mem_statSubmodule` 📖	mathematical	—	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.CrAnFieldOp` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `FieldStatistic.ofList` `FieldSpecification.crAnStatistics` `ofCrAnList`	—	—
`ofCrAnList_mem_statSubmodule_of_eq` 📖	mathematical	`FieldStatistic.ofList` `FieldSpecification.CrAnFieldOp` `FieldSpecification.crAnStatistics`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.fieldOpIdealSet` `statSubmodule` `ofCrAnList`	—	—

---

← Back to Index