OAI/NumberTheory/PrimePackets/RayFrobenius.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.GaloisIdealCharacter.primeAbove line 16
2. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.primeAbove_ne_bot line 20
3. def OAI.PrimeDegreePackets.GaloisIdealCharacter.primeFrobenius line 25
4. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.primeFrobenius_spec line 31
5. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.finite_factor_support line 40
6. def OAI.PrimeDegreePackets.GaloisIdealCharacter.idealHom line 55
7. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.idealHom_prime line 64
8. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.idealHom_finiteOrder line 75
9. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.idealHom_prime_frobenius line 90