OAI/NumberTheory/DirichletL/Hecke/Operations.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.HeckeFamily.Character.product line 9
  2. theorem OAI.SevenEighths.HeckeFamily.elementCoeff_product line 15
  3. def OAI.SevenEighths.HeckeFamily.Character.inverse line 19
  4. theorem OAI.SevenEighths.HeckeFamily.elementCoeff_inverse line 28
  5. def OAI.SevenEighths.HeckeFamily.Character.power line 32
  6. theorem OAI.SevenEighths.HeckeFamily.elementCoeff_power_of_unit line 46