OAI/NumberTheory/PrimePackets/FrobeniusConductor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.unramified_of_absDiscr_not_mem line 14
2. lemma OAI.PrimeDegreePackets.unramified_of_principal_congruence line 34
3. lemma OAI.PrimeDegreePackets.principal_count_ne_zero_iff_mem line 47
4. lemma OAI.PrimeDegreePackets.unramified_of_principal_count_ne_zero line 56
5. theorem OAI.PrimeDegreePackets.principal_congruence_frobenius_product line 67