OAI/NumberTheory/PrimePackets/AdelicAmbient.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.Adelic.finite_matrix_integral_mul line 11
  2. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteGL_one line 25
  3. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteGL_mul line 35
  4. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteGL_inv line 41
  5. def OAI.PrimeDegreePackets.Adelic.integralFiniteGroup line 46
  6. abbrev OAI.PrimeDegreePackets.Adelic.AdelicPGL line 52
  7. def OAI.PrimeDegreePackets.Adelic.rationalProjectiveEmbedding line 55
  8. def OAI.PrimeDegreePackets.Adelic.rationalProjectiveGroup line 59
  9. def OAI.PrimeDegreePackets.Adelic.finiteProjectiveIntegral line 62
  10. abbrev OAI.PrimeDegreePackets.Adelic.AmbientQuotient line 67
  11. def OAI.PrimeDegreePackets.Adelic.realAmbientPoint line 70
  12. lemma OAI.PrimeDegreePackets.Adelic.specialLinear_toPGL_injective_odd line 74
  13. lemma OAI.PrimeDegreePackets.Adelic.specialLinear_toPGL_surjective_odd line 88
  14. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteGL_scalar line 113
  15. lemma OAI.PrimeDegreePackets.Adelic.rational_gl_of_finite_integral line 127
  16. lemma OAI.PrimeDegreePackets.Adelic.projective_integral_real_lift line 161
  17. lemma OAI.PrimeDegreePackets.Adelic.rational_projective_integral_lift line 184
  18. lemma OAI.PrimeDegreePackets.Adelic.integralFiniteGL_int_matrix line 218
  19. lemma OAI.PrimeDegreePackets.Adelic.realAmbientPoint_eq_iff line 231
  20. lemma OAI.PrimeDegreePackets.Adelic.realAmbientPoint_surjective line 276
  21. theorem OAI.PrimeDegreePackets.Adelic.ambient_quotient_equiv line 301