OAI/NumberTheory/PrimePackets/RayUnramified.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classRay_allCoefficient line 15
  2. def OAI.PrimeDegreePackets.EvenRayCharacter.badPrimes line 23
  3. lemma OAI.PrimeDegreePackets.EvenRayCharacter.mem_badPrimes line 25
  4. def OAI.PrimeDegreePackets.EvenRayCharacter.classEulerCorrection line 34
  5. def OAI.PrimeDegreePackets.EvenRayCharacter.badEulerCorrection line 38
  6. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classEulerCorrection_ne_zero line 41
  7. lemma OAI.PrimeDegreePackets.EvenRayCharacter.badEulerCorrection_ne_zero line 63
  8. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classEulerCorrection_entire line 67
  9. lemma OAI.PrimeDegreePackets.EvenRayCharacter.badEulerCorrection_entire line 77
  10. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classEulerCorrection_inv line 81
  11. lemma OAI.PrimeDegreePackets.EvenRayCharacter.local_euler_of_residue_one line 91
  12. theorem OAI.PrimeDegreePackets.EvenRayCharacter.dirichlet_of_residue_one line 120
  13. def OAI.PrimeDegreePackets.EvenRayCharacter.unramifiedContinued line 143
  14. lemma OAI.PrimeDegreePackets.EvenRayCharacter.unramifiedContinued_entire line 149
  15. theorem OAI.PrimeDegreePackets.EvenRayCharacter.unramifiedContinued_eq_dirichlet line 154
  16. lemma OAI.PrimeDegreePackets.EvenRayCharacter.unramifiedContinued_ne_zero line 161
  17. theorem OAI.PrimeDegreePackets.EvenRayCharacter.unramifiedContinued_order line 172
  18. theorem OAI.PrimeDegreePackets.EvenRayCharacter.unramifiedContinued_finite_nonnegative_order line 186