OAI/NumberTheory/PrimePackets/PermutationArtin.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PrimeDegreePackets.GaloisIdealCharacter.additiveCharEquiv line 15
2. def OAI.PrimeDegreePackets.GaloisIdealCharacter.complexMulBasis line 20
3. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.complexMulBasis_apply line 24
4. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.det_eq_prod_of_eigenbasis line 30
5. abbrev OAI.PrimeDegreePackets.GaloisIdealCharacter.orbitQuotient line 45
6. def OAI.PrimeDegreePackets.GaloisIdealCharacter.orbitFunctionEquiv line 51
7. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.orbitFunctionEquiv_apply line 57
8. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.orbitFunctionEquiv_translate line 62
9. def OAI.PrimeDegreePackets.GaloisIdealCharacter.orbitCharacterBasis line 70
10. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.orbitCharacterBasis_eigen line 73
11. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.generator_quotient line 91
12. lemma OAI.PrimeDegreePackets.GaloisIdealCharacter.det_translate line 99
13. theorem OAI.PrimeDegreePackets.GaloisIdealCharacter.actual_nonnormal_artin_localEuler line 130