OAI/NumberTheory/PrimePackets/ArtinEuler.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.prod_one_sub_rootsOfUnity line 12
2. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.prod_comp_surjective_hom line 47
3. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.zpowers_subtype_generator line 58
4. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.prod_characters_at_generator line 65
5. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.prod_characters_at_element line 78
6. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.actual_cyclic_artin_localEuler line 104