OAI/RepresentationTheory/VertexAlgebra/ModuleCreationVacuum.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.creationVacuumCoefficientline 14 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.creationVacuumCoefficient_zeroline 17 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.creationVacuumCoefficient_eq_creationModeline 21 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.creationVacuumCoefficient_normline 30 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.creationVacuumSeries_summableline 52 - theorem
OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.creationVacuumSmear_summableline 66