OAI/NumberTheory/PrimePackets/AdelicDescent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.Adelic.adelicRegular_principal line 11
2. lemma OAI.PrimeDegreePackets.Adelic.adelicRegular_scalar line 29
3. lemma OAI.PrimeDegreePackets.Adelic.adelicRegular_mem_rational_of_principalScalar line 44
4. def OAI.PrimeDegreePackets.Adelic.adelicIdelePoint line 59
5. lemma OAI.PrimeDegreePackets.Adelic.adelicIdelePoint_mul_principalScalar line 67
6. def OAI.PrimeDegreePackets.Adelic.adelicTorusPoint line 82
7. instance OAI.PrimeDegreePackets.Adelic.torusQuotientMeasurable line 93
8. instance OAI.PrimeDegreePackets.Adelic.torusQuotientBorel line 95