OAI/NumberTheory/PrimePackets/FrobeniusCoset.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.zpowers_frobenius_eq_stabilizer line 14
2. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.under_fixing_smul line 43
3. def OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetPrime line 49
4. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetPrime_mk line 59
5. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetPrime_stabilizer_smul line 64
6. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.mem_coset_stabilizer_iff line 79
7. def OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetStabilizerEquiv line 90
8. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetPrime_eq_iff line 115
9. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetPrime_mem_primesOver line 143
10. def OAI.PrimeDegreePackets.GaloisIdealCharacter.primeOfCosetOrbit line 156
11. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.primeOfCosetOrbit_bijective line 166
12. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.cosetOrbit_card_eq_inertiaDeg line 193
13. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.actual_frobenius_coset_cycle_lengths line 246