OAI/NumberTheory/DirichletL/ConductorPresentation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.FiniteConductor.FactorsThroughIdeal.bot line 12
  2. theorem OAI.SevenEighths.FiniteConductor.FactorsThroughIdeal.pow line 18
  3. def OAI.SevenEighths.ConductorPresentation.quotientCharacter line 37
  4. theorem OAI.SevenEighths.ConductorPresentation.quotientCharacter_mk line 41
  5. theorem OAI.SevenEighths.ConductorPresentation.primitive_quotientCharacter line 46
  6. theorem OAI.SevenEighths.ConductorPresentation.source_le_comap line 51
  7. theorem OAI.SevenEighths.ConductorPresentation.unit_factorization_of_mask line 58
  8. theorem OAI.SevenEighths.ConductorPresentation.comap_ne_bot line 77
  9. theorem OAI.SevenEighths.ConductorPresentation.exists_primitive_presentation_above_quotient line 88
  10. theorem OAI.SevenEighths.ConductorPresentation.exists_primitive_presentation line 104
  11. theorem OAI.SevenEighths.ConductorPresentation.exists_primitive_presentation_above line 115
  12. theorem OAI.SevenEighths.ConductorPresentation.exists_primitive_product_presentation line 126
  13. theorem OAI.SevenEighths.ConductorPresentation.exists_primitive_power_presentation line 148