OAI/RepresentationTheory/VertexAlgebra/MobiusRepresentation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StronglyRationalVOA.phaseUnitary line 13
  2. lemma OAI.StronglyRationalVOA.phaseUnitary_apply line 17
  3. lemma OAI.StronglyRationalVOA.projective_eq_of_phase line 19
  4. lemma OAI.StronglyRationalVOA.projective_eq_vacuum_unique line 27
  5. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.completion_vacuum_norm line 47
  6. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.completion_vacuum_ne_zero line 50
  7. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusVacuumPhase line 56
  8. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusVacuumPhase_spec line 58
  9. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusVacuumPhase_norm line 66
  10. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusVacuumPhase_ne_zero line 71
  11. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusLiftUnitary line 78
  12. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusLiftUnitary_apply line 82
  13. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusLiftUnitary_vacuum line 85
  14. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusLiftUnitary_projective line 89
  15. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusLiftUnitary_mul line 94
  16. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusLiftRepresentation line 103
  17. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusLiftRepresentation_kernel line 106
  18. def OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusRepresentation line 120
  19. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusRepresentation_vacuum line 124
  20. lemma OAI.StronglyRationalVOA.CFTTypeVOA.UnitaryStructure.mobiusRepresentation_projective line 128