OAI/NumberTheory/DirichletL/Hecke/Family.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.HeckeFamily.K line 13

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

2. abbrev OAI.SevenEighths.HeckeFamily.O line 14

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

3. instance OAI.SevenEighths.HeckeFamily.(instance at line 16) line 16
4. def OAI.SevenEighths.HeckeFamily.omega line 18

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

5. def OAI.SevenEighths.HeckeFamily.coordinateElement line 20

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

6. structure OAI.SevenEighths.HeckeFamily.Character line 22

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

7. def OAI.SevenEighths.HeckeFamily.Character.ofResidue line 31
8. instance OAI.SevenEighths.HeckeFamily.(instance at line 46) line 46
9. def OAI.SevenEighths.HeckeFamily.elementCoeff line 48

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

10. def OAI.SevenEighths.HeckeFamily.coefficients line 50

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

11. theorem OAI.SevenEighths.HeckeFamily.elementCoeff_one line 53
12. theorem OAI.SevenEighths.HeckeFamily.elementCoeff_mul line 56
13. theorem OAI.SevenEighths.HeckeFamily.elementCoeff_unit_mul line 60
14. theorem OAI.SevenEighths.HeckeFamily.quotient_period line 66
15. theorem OAI.SevenEighths.HeckeFamily.elementCoeff_add_period_mul line 70
16. theorem OAI.SevenEighths.HeckeFamily.periodicCoeff_eq_elementCoeff line 74
17. def OAI.SevenEighths.HeckeFamily.continuedLattice line 91

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

18. theorem OAI.SevenEighths.HeckeFamily.continuedLattice_differentiableAt line 93