OAI/NumberTheory/Ostmann/Characters/DiagonalEstimateCopiedCodesBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Ostmann.Characters.DiagonalEstimate.ActualCopied line 13
  2. def OAI.Ostmann.Characters.DiagonalEstimate.IsCopiedBulk line 16
  3. abbrev OAI.Ostmann.Characters.DiagonalEstimate.CopiedNonbulk line 20
  4. def OAI.Ostmann.Characters.DiagonalEstimate.copiedBulk line 23
  5. theorem OAI.Ostmann.Characters.DiagonalEstimate.copiedBulk_isBulk line 29
  6. def OAI.Ostmann.Characters.DiagonalEstimate.copiedBulkEquiv line 33
  7. def OAI.Ostmann.Characters.DiagonalEstimate.copiedBulkNonbulkEquiv line 41
  8. theorem OAI.Ostmann.Characters.DiagonalEstimate.copiedBulkNonbulkEquiv_bulk line 46
  9. theorem OAI.Ostmann.Characters.DiagonalEstimate.copiedBulkNonbulkEquiv_nonbulk line 54
  10. theorem OAI.Ostmann.Characters.DiagonalEstimate.copied_top_nonbulk line 61