OAI/NumberTheory/DirichletL/ResidueCharacter.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ResidueCharacter.inflate line 15
  2. theorem OAI.SevenEighths.ResidueCharacter.inflate_toUnitHom line 20
  3. theorem OAI.SevenEighths.ResidueCharacter.inflate_apply_unit line 25
  4. theorem OAI.SevenEighths.ResidueCharacter.inflate_apply line 30
  5. theorem OAI.SevenEighths.ResidueCharacter.inflate_mk line 38
  6. theorem OAI.SevenEighths.ResidueCharacter.inflate_factorsThrough line 43
  7. theorem OAI.SevenEighths.ResidueCharacter.inflate_trans line 56
  8. theorem OAI.SevenEighths.ResidueCharacter.inflate_global_units line 67
  9. theorem OAI.SevenEighths.ResidueCharacter.isUnit_mk_inf_iff line 74
  10. theorem OAI.SevenEighths.ResidueCharacter.finite_quotient_inf line 101
  11. def OAI.SevenEighths.ResidueCharacter.product line 113
  12. theorem OAI.SevenEighths.ResidueCharacter.product_mk line 117
  13. theorem OAI.SevenEighths.ResidueCharacter.product_global_units line 131
  14. theorem OAI.SevenEighths.ResidueCharacter.exists_primitive_product line 143
  15. theorem OAI.SevenEighths.ResidueCharacter.exists_primitive_product_global_units line 158