OAI/NumberTheory/DirichletL/IdealCharacter.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.IdealCharacter.UnitInvariant line 17
  2. theorem OAI.SevenEighths.IdealCharacter.residue_eq_of_associated line 20
  3. theorem OAI.SevenEighths.IdealCharacter.isUnit_mk_iff_isCoprime line 26
  4. def OAI.SevenEighths.IdealCharacter.value line 48
  5. theorem OAI.SevenEighths.IdealCharacter.value_bot line 52
  6. theorem OAI.SevenEighths.IdealCharacter.value_span line 55
  7. def OAI.SevenEighths.IdealCharacter.ofResidue line 63
  8. theorem OAI.SevenEighths.IdealCharacter.ofResidue_bot line 92
  9. theorem OAI.SevenEighths.IdealCharacter.ofResidue_span line 95
  10. theorem OAI.SevenEighths.IdealCharacter.ofResidue_of_generator line 100
  11. theorem OAI.SevenEighths.IdealCharacter.norm_residue_le_one line 111
  12. theorem OAI.SevenEighths.IdealCharacter.norm_ofResidue_le_one line 123
  13. theorem OAI.SevenEighths.IdealCharacter.one_unitInvariant line 135
  14. theorem OAI.SevenEighths.IdealCharacter.ofResidue_one line 139
  15. theorem OAI.SevenEighths.IdealCharacter.ofResidue_one_top line 157
  16. theorem OAI.SevenEighths.IdealCharacter.ofResidue_source_mask line 163
  17. theorem OAI.SevenEighths.IdealCharacter.ofResidue_finite_deletion line 180
  18. theorem OAI.SevenEighths.IdealCharacter.ofResidue_product line 194
  19. theorem OAI.SevenEighths.IdealCharacter.exists_primitive_associate line 212
  20. theorem OAI.SevenEighths.IdealCharacter.exists_primitive_product_associate line 229