OAI/NumberTheory/DirichletL/Hecke/UnitRows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.HeckeUnitRows.seven_coprime_thirty_six line 16
  2. theorem OAI.SevenEighths.HeckeUnitRows.supported_unit_thirty_six line 24
  3. theorem OAI.SevenEighths.HeckeUnitRows.unitSupplement_unit line 34
  4. theorem OAI.SevenEighths.HeckeUnitRows.unitSupplement_factorsModulo line 44
  5. def OAI.SevenEighths.HeckeUnitRows.character line 48
  6. theorem OAI.SevenEighths.HeckeUnitRows.elementCoeff_character line 53
  7. theorem OAI.SevenEighths.HeckeUnitRows.seven_supported line 61
  8. theorem OAI.SevenEighths.HeckeUnitRows.unitSupplement_seven line 73
  9. theorem OAI.SevenEighths.HeckeUnitRows.character_nonprincipal line 83
  10. theorem OAI.SevenEighths.HeckeUnitRows.masked_character_nonprincipal line 99