OAI/NumberTheory/PrimePackets/MonomialArtin.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PrimeDegreePackets.ArtinInduction.unitCharacterRep line 12
  2. def OAI.PrimeDegreePackets.ArtinInduction.cosetRemainder line 20
  3. lemma OAI.PrimeDegreePackets.ArtinInduction.cosetRemainder_mul line 25
  4. def OAI.PrimeDegreePackets.ArtinInduction.coindCosetEquiv line 33
  5. lemma OAI.PrimeDegreePackets.ArtinInduction.coindCosetEquiv_apply line 63
  6. lemma OAI.PrimeDegreePackets.ArtinInduction.coindCosetEquiv_symm_apply line 66
  7. def OAI.PrimeDegreePackets.ArtinInduction.cosetMonomialRep line 70
  8. def OAI.PrimeDegreePackets.ArtinInduction.cosetWeight line 74
  9. lemma OAI.PrimeDegreePackets.ArtinInduction.cosetMonomialRep_apply line 77
  10. def OAI.PrimeDegreePackets.ArtinInduction.Spectral.stabilizerWeight line 99
  11. def OAI.PrimeDegreePackets.ArtinInduction.Spectral.project line 113
  12. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.project_eigen line 117
  13. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.project_single_at line 130
  14. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.project_single_ne_zero line 153
  15. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.character_eval_generator_injective line 161
  16. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.quotient_generator line 172
  17. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.exists_transitive_eigenbasis line 182
  18. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.transitive_det line 233
  19. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.weight_one line 301
  20. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.weight_mul line 308
  21. def OAI.PrimeDegreePackets.ArtinInduction.Spectral.orbitRep line 317
  22. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.orbitRep_apply line 339
  23. def OAI.PrimeDegreePackets.ArtinInduction.Spectral.orbitFunctionEquiv line 342
  24. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.orbitFunctionEquiv_apply line 347
  25. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.orbitFunctionEquiv_intertwine line 352
  26. def OAI.PrimeDegreePackets.ArtinInduction.Spectral.orbitAnchor line 359
  27. lemma OAI.PrimeDegreePackets.ArtinInduction.Spectral.det_monomial line 363
  28. lemma OAI.PrimeDegreePackets.ArtinInduction.actual_frobenius_coset_primes line 435
  29. lemma OAI.PrimeDegreePackets.ArtinInduction.actual_coset_weight line 458
  30. theorem OAI.PrimeDegreePackets.ArtinInduction.actual_monomial_artin_localEuler line 535