OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticResidueSplit.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Constructing the support data from an actual residue numerator

  1. structure OAI.Ostmann.ArithmeticResidueSplit line 14

    Source documentation

    The two coefficients contain the current giant and its nonbulk factors. They are allowed to fail the required unit tests.

    structure ArithmeticResidueSplit (Q : ℕ) where
…
  2. def OAI.Ostmann.ArithmeticResidueSplit.reduce line 22
  3. def OAI.Ostmann.ArithmeticResidueSplit.numerator line 26
  4. def OAI.Ostmann.ArithmeticResidueSplit.support line 31
  5. def OAI.Ostmann.ArithmeticResidueSplit.toData line 36
  6. theorem OAI.Ostmann.ArithmeticResidueSplit.toData_frequencies line 52
  7. theorem OAI.Ostmann.ArithmeticResidueSplit.toData_test line 60
  8. def OAI.Ostmann.arithmeticResiduePairData line 86
  9. theorem OAI.Ostmann.arithmeticResiduePairData_test line 92
  10. theorem OAI.Ostmann.arithmeticResiduePairData_frequencies line 101