OAI/RepresentationTheory/VertexAlgebra/ModuleSharpNormalProducts.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.ColumnControl line 13
  2. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.columnControl_subset line 20
  3. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.AdjointColumnControl line 30
  4. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.adjointColumnControl_subset line 34
  5. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.normalLeft line 46
  6. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.normalRightHigh line 50
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.normalRightLow line 54
  8. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalLeft_mem_cutoff line 61
  9. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalRightHigh_mem_cutoff line 72
  10. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalRightLow_mem_cutoff line 81
  11. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalLeft_sq_le line 90
  12. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalRightHigh_sq_le line 111
  13. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalRightLow_column_sq_le line 144
  14. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normal_product_cutoff_split line 179
  15. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.singular_correction_column_sq_le line 215
  16. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.columnControl_mono line 246
  17. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.columnControl_mode_sq_le line 254
  18. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalProduct_columnControl line 259
  19. theorem OAI.StronglyRationalVOA.CFTTypeVOA.GradingRestrictedModule.UnitaryStructure.normalProduct_zero_sq_le line 298