OAI/NumberTheory/PrimePackets/AdelicFinal.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.Adelic.packetOrbits_eq_of_carrier line 13
2. lemma OAI.PrimeDegreePackets.Adelic.packetMeasure_eq_of_carrier line 19
3. lemma OAI.PrimeDegreePackets.Adelic.packetSupport_eq_of_carrier line 25
4. theorem OAI.PrimeDegreePackets.Adelic.every_local_type_adelic_realization line 31
5. theorem OAI.PrimeDegreePackets.Adelic.adelic_packet_main line 53