OAI/NumberTheory/DirichletL/Hecke/IdealBridge.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SevenEighths.HeckeFamily.(instance at line 12) line 12
  2. def OAI.SevenEighths.HeckeFamily.idealCoeff line 14
  3. theorem OAI.SevenEighths.HeckeFamily.idealCoeff_zero line 17
  4. theorem OAI.SevenEighths.HeckeFamily.idealCoeff_span line 19
  5. theorem OAI.SevenEighths.HeckeFamily.coordinateElement_eq_baseline line 23
  6. def OAI.SevenEighths.HeckeFamily.coordinateEquiv line 26
  7. theorem OAI.SevenEighths.HeckeFamily.normForm_eq_absNorm_span line 33
  8. def OAI.SevenEighths.HeckeFamily.elementTerm line 41
  9. def OAI.SevenEighths.HeckeFamily.idealTerm line 44
  10. theorem OAI.SevenEighths.HeckeFamily.elementTerm_coordinate line 47
  11. theorem OAI.SevenEighths.HeckeFamily.elementTerm_hasSum line 56
  12. theorem OAI.SevenEighths.HeckeFamily.elementTerm_zero line 62
  13. theorem OAI.SevenEighths.HeckeFamily.elementTerm_unit_mul line 66
  14. theorem OAI.SevenEighths.HeckeFamily.elementTerm_idealGenerator line 71
  15. theorem OAI.SevenEighths.HeckeFamily.continuedLattice_eq_six_ideal_tsum line 80
  16. def OAI.SevenEighths.HeckeFamily.LFunction line 95

    Also declared: ComparatorChallenges/HeckeSevenEighths.lean:235 (same declaration text).

  17. theorem OAI.SevenEighths.HeckeFamily.LFunction_eq_ideal_tsum line 97
  18. theorem OAI.SevenEighths.HeckeFamily.LFunction_differentiableAt line 102
  19. theorem OAI.SevenEighths.HeckeFamily.LFunction_entire_nonprincipal line 110