Grading

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

Statistics

Metric	Count
Definitions bosonicProjF, fermionicProjF, fieldOpFreeAlgebraGrade, statisticSubmodule	4
Theorems bosonicProjF_add_fermionicProjF, bosonicProjF_mul, bosonicProjF_ofCrAnListF, bosonicProjF_of_bonosic_part, bosonicProjF_of_fermionic_part, bosonicProjF_of_mem_bosonic, bosonicProjF_of_mem_fermionic, coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, directSum_eq_bosonic_plus_fermionic, eq_zero_of_bosonic_and_fermionic, fermionicProjF_mul, fermionicProjF_ofCrAnListF, fermionicProjF_ofCrAnListF_if_bosonic, fermionicProjF_of_bosonic_part, fermionicProjF_of_fermionic_part, fermionicProjF_of_mem_bosonic, fermionicProjF_of_mem_fermionic, ofCrAnListF_bosonic_or_fermionic, ofCrAnListF_mem_statisticSubmodule_of, ofCrAnOpF_bosonic_or_fermionic	20
Total	24

FieldSpecification.FieldOpFreeAlgebra

Definitions

Name	Category	Theorems
bosonicProjF 📖	CompOp	13 math math: superCommuteF_expand_bosonicProjF_fermionicProjF, FieldSpecification.WickAlgebra.bosonicProjF_mem_ideal, fermionicProjF_mul, bosonicProjF_of_mem_bosonic, bosonicProjF_of_fermionic_part, FieldSpecification.WickAlgebra.ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero, FieldSpecification.WickAlgebra.bosonicProjF_mem_fieldOpIdealSet_or_zero, FieldSpecification.WickAlgebra.bosonicProjFree_eq_ι_bosonicProjF, bosonicProjF_of_bonosic_part, bosonicProjF_mul, bosonicProjF_of_mem_fermionic, bosonicProjF_add_fermionicProjF, bosonicProjF_ofCrAnListF
fermionicProjF 📖	CompOp	14 math math: superCommuteF_expand_bosonicProjF_fermionicProjF, FieldSpecification.WickAlgebra.fermionicProjFree_eq_ι_fermionicProjF, fermionicProjF_mul, fermionicProjF_of_mem_fermionic, fermionicProjF_ofCrAnListF, FieldSpecification.WickAlgebra.ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero, FieldSpecification.WickAlgebra.fermionicProjF_mem_fieldOpIdealSet_or_zero, fermionicProjF_ofCrAnListF_if_bosonic, fermionicProjF_of_mem_bosonic, fermionicProjF_of_bosonic_part, FieldSpecification.WickAlgebra.fermionicProjF_mem_ideal, fermionicProjF_of_fermionic_part, bosonicProjF_mul, bosonicProjF_add_fermionicProjF
fieldOpFreeAlgebraGrade 📖	CompOp	—
statisticSubmodule 📖	CompOp	27 math math: superCommuteF_expand_bosonicProjF_fermionicProjF, FieldSpecification.WickAlgebra.bosonicProjF_mem_ideal, FieldSpecification.WickAlgebra.fermionicProjFree_eq_ι_fermionicProjF, fermionicProjF_mul, coeAddMonoidHom_apply_eq_bosonic_plus_fermionic, ofCrAnOpF_bosonic_or_fermionic, directSum_eq_bosonic_plus_fermionic, superCommuteF_ofCrAnListF_ofCrAnListF_bosonic_or_fermionic, superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_fermionic, ofCrAnListF_mem_statisticSubmodule_of, bosonicProjF_of_fermionic_part, fermionicProjF_ofCrAnListF, FieldSpecification.WickAlgebra.ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero, FieldSpecification.WickAlgebra.fermionicProjF_mem_fieldOpIdealSet_or_zero, fermionicProjF_ofCrAnListF_if_bosonic, FieldSpecification.WickAlgebra.bosonicProjF_mem_fieldOpIdealSet_or_zero, FieldSpecification.WickAlgebra.bosonicProjFree_eq_ι_bosonicProjF, fermionicProjF_of_bosonic_part, superCommuteF_superCommuteF_ofCrAnOpF_bosonic_or_fermionic, ofCrAnListF_bosonic_or_fermionic, FieldSpecification.WickAlgebra.fermionicProjF_mem_ideal, bosonicProjF_of_bonosic_part, fermionicProjF_of_fermionic_part, bosonicProjF_mul, FieldSpecification.WickAlgebra.ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_bosonic_or_zero, bosonicProjF_add_fermionicProjF, bosonicProjF_ofCrAnListF

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bosonicProjF_add_fermionicProjF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic bosonicProjF FieldStatistic.fermionic fermionicProjF	—	ofListBasis_eq_ofList bosonicProjF_ofCrAnListF fermionicProjF_ofCrAnListF_if_bosonic
bosonicProjF_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic bosonicProjF FieldStatistic.fermionic fermionicProjF	—	bosonicProjF_add_fermionicProjF FieldStatistic.mul_self bosonicProjF_of_mem_bosonic bosonicProjF_of_mem_fermionic FieldStatistic.mul_bosonic
bosonicProjF_ofCrAnListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic bosonicProjF ofCrAnListF FieldStatistic FieldStatistic.ofList FieldSpecification.crAnStatistics instDecidableEqFieldStatistic	—	ofListBasis_eq_ofList bosonicProjF.eq_1
bosonicProjF_of_bonosic_part 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic bosonicProjF FieldStatistic	—	bosonicProjF_of_mem_bosonic
bosonicProjF_of_fermionic_part 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic bosonicProjF FieldStatistic.fermionic FieldStatistic	—	bosonicProjF_of_mem_fermionic
bosonicProjF_of_mem_bosonic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic	bosonicProjF	—	bosonicProjF_ofCrAnListF
bosonicProjF_of_mem_fermionic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic	FieldStatistic.bosonic bosonicProjF	—	bosonicProjF_ofCrAnListF
coeAddMonoidHom_apply_eq_bosonic_plus_fermionic 📖	mathematical	—	FieldStatistic FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule instDecidableEqFieldStatistic FieldStatistic.bosonic FieldStatistic.fermionic	—	—
directSum_eq_bosonic_plus_fermionic 📖	mathematical	—	FieldStatistic FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic instDecidableEqFieldStatistic FieldStatistic.fermionic	—	—
eq_zero_of_bosonic_and_fermionic 📖	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic FieldStatistic.fermionic	—	—	bosonicProjF_of_mem_bosonic fermionicProjF_of_mem_fermionic bosonicProjF_add_fermionicProjF
fermionicProjF_mul 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic fermionicProjF FieldStatistic.bosonic bosonicProjF	—	bosonicProjF_add_fermionicProjF fermionicProjF_of_mem_bosonic FieldStatistic.mul_self FieldStatistic.mul_bosonic fermionicProjF_of_mem_fermionic
fermionicProjF_ofCrAnListF 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic fermionicProjF ofCrAnListF FieldStatistic FieldStatistic.ofList FieldSpecification.crAnStatistics instDecidableEqFieldStatistic	—	ofListBasis_eq_ofList fermionicProjF.eq_1
fermionicProjF_ofCrAnListF_if_bosonic 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic fermionicProjF ofCrAnListF FieldStatistic FieldStatistic.ofList FieldSpecification.crAnStatistics FieldStatistic.bosonic instDecidableEqFieldStatistic	—	fermionicProjF_ofCrAnListF
fermionicProjF_of_bosonic_part 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic fermionicProjF FieldStatistic.bosonic FieldStatistic	—	fermionicProjF_of_mem_bosonic
fermionicProjF_of_fermionic_part 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic fermionicProjF FieldStatistic	—	fermionicProjF_of_mem_fermionic
fermionicProjF_of_mem_bosonic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic	FieldStatistic.fermionic fermionicProjF	—	fermionicProjF_ofCrAnListF
fermionicProjF_of_mem_fermionic 📖	mathematical	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.fermionic	fermionicProjF	—	fermionicProjF_ofCrAnListF
ofCrAnListF_bosonic_or_fermionic 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic ofCrAnListF FieldStatistic.fermionic	—	ofCrAnListF_mem_statisticSubmodule_of
ofCrAnListF_mem_statisticSubmodule_of 📖	mathematical	FieldStatistic.ofList FieldSpecification.CrAnFieldOp FieldSpecification.crAnStatistics	FieldSpecification.FieldOpFreeAlgebra statisticSubmodule ofCrAnListF	—	—
ofCrAnOpF_bosonic_or_fermionic 📖	mathematical	—	FieldSpecification.FieldOpFreeAlgebra FieldSpecification.CrAnFieldOp statisticSubmodule FieldStatistic.bosonic ofCrAnOpF FieldStatistic.fermionic	—	ofCrAnListF_singleton ofCrAnListF_bosonic_or_fermionic

---

← Back to Index