OAI/NumberTheory/PrimePackets/RayCharacter.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.quotient_isUnit_iff_span_coprime line 14
  2. structure OAI.PrimeDegreePackets.EvenRayCharacter line 44
  3. lemma OAI.PrimeDegreePackets.EvenRayCharacter.idealHom_norm line 57
  4. lemma OAI.PrimeDegreePackets.EvenRayCharacter.residue_unit line 66
  5. def OAI.PrimeDegreePackets.EvenRayCharacter.underlyingIdeal line 77
  6. lemma OAI.PrimeDegreePackets.EvenRayCharacter.underlyingIdeal_ne_bot line 80
  7. lemma OAI.PrimeDegreePackets.EvenRayCharacter.underlyingIdeal_coe line 83
  8. lemma OAI.PrimeDegreePackets.EvenRayCharacter.underlyingIdeal_unit line 88
  9. lemma OAI.PrimeDegreePackets.EvenRayCharacter.generator_principal_product line 95
  10. lemma OAI.PrimeDegreePackets.EvenRayCharacter.generator_integer_ne_zero line 118
  11. lemma OAI.PrimeDegreePackets.EvenRayCharacter.generator_fractional_product line 127
  12. def OAI.PrimeDegreePackets.EvenRayCharacter.coefficient line 141
  13. lemma OAI.PrimeDegreePackets.EvenRayCharacter.coefficient_norm_le_one line 145
  14. lemma OAI.PrimeDegreePackets.EvenRayCharacter.coefficient_eq_residue line 155
  15. def OAI.PrimeDegreePackets.EvenRayCharacter.dirichlet line 180
  16. lemma OAI.PrimeDegreePackets.EvenRayCharacter.dirichlet_summable line 184
  17. def OAI.PrimeDegreePackets.EvenRayCharacter.classIdeal line 196
  18. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classIdeal_ne_bot line 201
  19. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classIdeal_coprime line 205
  20. lemma OAI.PrimeDegreePackets.EvenRayCharacter.classIdeal_class line 209
  21. def OAI.PrimeDegreePackets.EvenRayCharacter.classPartition line 218
  22. def OAI.PrimeDegreePackets.EvenRayCharacter.continued line 242
  23. theorem OAI.PrimeDegreePackets.EvenRayCharacter.continued_entire line 251
  24. theorem OAI.PrimeDegreePackets.EvenRayCharacter.continued_eq_dirichlet line 263
  25. lemma OAI.PrimeDegreePackets.EvenRayCharacter.coefficient_unit line 287
  26. theorem OAI.PrimeDegreePackets.EvenRayCharacter.dirichlet_tendsto_atTop line 307
  27. lemma OAI.PrimeDegreePackets.EvenRayCharacter.continued_tendsto_atTop line 338
  28. lemma OAI.PrimeDegreePackets.EvenRayCharacter.continued_ne_zero line 346
  29. theorem OAI.PrimeDegreePackets.EvenRayCharacter.continued_finite_nonnegative_order line 355
  30. def OAI.PrimeDegreePackets.EvenRayCharacter.conjugate line 372
  31. lemma OAI.PrimeDegreePackets.EvenRayCharacter.conjugate_idealHom line 386
  32. lemma OAI.PrimeDegreePackets.EvenRayCharacter.conjugate_residue_ne_one line 390
  33. lemma OAI.PrimeDegreePackets.EvenRayCharacter.coefficient_conjugate line 398
  34. lemma OAI.PrimeDegreePackets.EvenRayCharacter.dirichlet_conj_real line 406
  35. theorem OAI.PrimeDegreePackets.EvenRayCharacter.continued_conjugation line 418
  36. lemma OAI.PrimeDegreePackets.EvenRayCharacter.analyticAt_reflection line 437
  37. lemma OAI.PrimeDegreePackets.EvenRayCharacter.iteratedDeriv_reflection line 445
  38. lemma OAI.PrimeDegreePackets.EvenRayCharacter.analyticOrderAt_reflection line 451
  39. theorem OAI.PrimeDegreePackets.EvenRayCharacter.continued_order_conjugation line 462