OAI/NumberTheory/PrimePackets/FrobeniusSurjective.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.GaloisIdealCharacter.coprimeFractionalIdeals line 13
  2. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.prime_mem_coprimeFractionalIdeals line 26
  3. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.frobenius_finite_factor_support line 40
  4. def OAI.PrimeDegreePackets.GaloisIdealCharacter.frobeniusHom line 54
  5. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.frobeniusHom_prime line 64
  6. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.character_comp_frobeniusHom line 74
  7. def OAI.PrimeDegreePackets.GaloisIdealCharacter.coprimeFrobeniusHom line 86
  8. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.coprimeFrobeniusHom_surjective line 93