OAI/RepresentationTheory/VertexAlgebra/ModuleBlockGrowth.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.BlockGrowth line 14
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.blockGrowth_zero line 18
  3. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.blockGrowth_add line 23
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.blockGrowth_smul line 40
  5. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.blockGrowth_mono_weight line 46
  6. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.translation_blockGrowth line 56
  7. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.finite_blockGrowth_uniform line 85
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.normalProduct_blockGrowth line 113
  9. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.blockGrowthSubmodule line 160
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.vacuum_blockGrowth line 167
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.homogeneousC2_le_blockGrowth line 174