OAI/NumberTheory/DirichletL/Hecke/LocalRamification.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.HeckeLocalRamification.crtCharacter_eq_one_iff line 13
  2. theorem OAI.SevenEighths.HeckeLocalRamification.primePowerCharacter_eq_one_iff line 49
  3. theorem OAI.SevenEighths.HeckeLocalRamification.canonicalPrimePowerCharacter_eq_one_iff line 72
  4. theorem OAI.SevenEighths.HeckeLocalRamification.canonicalCRTCharacter_eq_one_iff line 78
  5. theorem OAI.SevenEighths.HeckeLocalRamification.product_nonprincipal_of_coprime line 87
  6. theorem OAI.SevenEighths.HeckeLocalRamification.nonprincipal_fixed_times_local line 114