OAI/NumberTheory/DirichletL/Hecke/RowClosure.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.HeckeRowClosure.periodic_of_primary line 11
  2. def OAI.SevenEighths.HeckeRowClosure.quotientRow line 38
  3. theorem OAI.SevenEighths.HeckeRowClosure.quotientRow_mk line 46
  4. def OAI.SevenEighths.HeckeRowClosure.residueRow line 50
  5. theorem OAI.SevenEighths.HeckeRowClosure.residueRow_mk line 54
  6. def OAI.SevenEighths.HeckeRowClosure.rowCharacter line 68
  7. theorem OAI.SevenEighths.HeckeRowClosure.elementCoeff_rowCharacter line 75
  8. def OAI.SevenEighths.HeckeRowClosure.elementHom line 81
  9. theorem OAI.SevenEighths.HeckeRowClosure.elementHom_periodic line 86
  10. theorem OAI.SevenEighths.HeckeRowClosure.elementHom_norm line 92
  11. theorem OAI.SevenEighths.HeckeRowClosure.rowTwist_unit_mul line 97
  12. theorem OAI.SevenEighths.HeckeRowClosure.rowTwist_unit line 103
  13. theorem OAI.SevenEighths.HeckeRowClosure.rowTwist_periodic line 107
  14. theorem OAI.SevenEighths.HeckeRowClosure.rowTwist_nonzero_coprime line 130
  15. theorem OAI.SevenEighths.HeckeRowClosure.rowTwist_nonzero_unit line 147
  16. theorem OAI.SevenEighths.HeckeRowClosure.exists_row_character line 174
  17. def OAI.SevenEighths.HeckeRowClosure.rowConductorBound line 192
  18. theorem OAI.SevenEighths.HeckeRowClosure.row_modulus_norm_le line 196
  19. theorem OAI.SevenEighths.HeckeRowClosure.exists_row_character_with_conductor line 216
  20. theorem OAI.SevenEighths.HeckeRowClosure.idealCoeff_eq_row line 236
  21. theorem OAI.SevenEighths.HeckeRowClosure.exists_primitive_row line 251