OAI/NumberTheory/DirichletL/FiniteConductor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.FiniteConductor.exists_character_factor_iff line 18
  2. def OAI.SevenEighths.FiniteConductor.quotientUnits line 40
  3. def OAI.SevenEighths.FiniteConductor.FactorsThroughIdeal line 43
  4. theorem OAI.SevenEighths.FiniteConductor.quotientUnits_eq_one_iff line 48
  5. theorem OAI.SevenEighths.FiniteConductor.factorsThroughIdeal_iff line 53
  6. theorem OAI.SevenEighths.FiniteConductor.primitiveOnIdeals_iff_no_descent line 75
  7. theorem OAI.SevenEighths.FiniteConductor.FactorsThroughIdeal.mono line 81
  8. theorem OAI.SevenEighths.FiniteConductor.FactorsThroughIdeal.inv line 86
  9. theorem OAI.SevenEighths.FiniteConductor.factorization_with_source_mask line 94
  10. theorem OAI.SevenEighths.FiniteConductor.exists_primitive_quotient line 105
  11. theorem OAI.SevenEighths.FiniteConductor.exists_primitive_quotient_with_mask line 146