OAI/NumberTheory/PrimePackets/FrobeniusSplitting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.inertiaDeg_eq_one_of_one_isArithFrobAt line 14
2. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.inertiaDeg_eq_one_of_primeFrobenius_eq_one line 32
3. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.norm_eq_of_inertiaDeg_eq_one line 46
4. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.card_primesOver_of_unramified_of_inertia_one line 57
5. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.one_isArithFrobAt_kernelFixedField line 73
6. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.inertiaDeg_eq_one_kernelFixedField line 96