OAI/RepresentationTheory/VertexAlgebra/MobiusGroup.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.implements_one line 10
  2. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.implements_mul line 13
  3. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.implements_inv line 29
  4. def OAI.StronglyRationalVOA.CircleMobiusGeometry.lifts line 39
  5. def OAI.StronglyRationalVOA.CircleMobiusGeometry.rotationMatrix line 44
  6. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.implements_rotation line 48
  7. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.rotation_mem line 54
  8. def OAI.StronglyRationalVOA.CircleMobiusGeometry.rotation line 55
  9. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.rotation_zero line 56
  10. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.rotation_add line 57
  11. abbrev OAI.StronglyRationalVOA.CircleMobiusGeometry.Group line 61
  12. def OAI.StronglyRationalVOA.CircleMobiusGeometry.inclusion line 63
  13. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.inclusion_injective line 68
  14. lemma OAI.StronglyRationalVOA.CircleMobiusGeometry.inclusion_continuous line 76