OAI/Computability/DeterministicSum/ModularInverses.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Costed modular powers, inverses and common-denominator tables.

  1. def OAI.DeterministicThreeSum.Structured.ModularPower.bit line 11
  2. def OAI.DeterministicThreeSum.Structured.ModularPower.conditional line 12
  3. def OAI.DeterministicThreeSum.Structured.ModularPower.square line 13
  4. def OAI.DeterministicThreeSum.Structured.ModularPower.step line 15
  5. def OAI.DeterministicThreeSum.Structured.ModularPower.loop line 16
  6. def OAI.DeterministicThreeSum.Structured.ModularPower.nextAcc line 18
  7. def OAI.DeterministicThreeSum.Structured.ModularPower.nextState line 20
  8. lemma OAI.DeterministicThreeSum.Structured.ModularPower.conditional_correct line 23
  9. lemma OAI.DeterministicThreeSum.Structured.ModularPower.step_correct line 42
  10. lemma OAI.DeterministicThreeSum.Structured.ModularPower.nextAcc_lt line 64
  11. lemma OAI.DeterministicThreeSum.Structured.ModularPower.next_cast line 70
  12. theorem OAI.DeterministicThreeSum.Structured.ModularPower.loop_correct line 83
  13. def OAI.DeterministicThreeSum.Structured.ModularPower.inverseSetup line 119
  14. def OAI.DeterministicThreeSum.Structured.ModularPower.inverse line 122
  15. lemma OAI.DeterministicThreeSum.Structured.ModularPower.prime_power_totient line 124
  16. lemma OAI.DeterministicThreeSum.Structured.ModularPower.inverseSetup_correct line 129
  17. lemma OAI.DeterministicThreeSum.Structured.ModularPower.euler_inverse line 145
  18. theorem OAI.DeterministicThreeSum.Structured.ModularPower.inverse_correct line 155
  19. def OAI.DeterministicThreeSum.Structured.Indexed.integerInverse line 182
  20. lemma OAI.DeterministicThreeSum.Structured.Indexed.integerValue_nat line 185
  21. lemma OAI.DeterministicThreeSum.Structured.Indexed.coprime_remainder line 187
  22. theorem OAI.DeterministicThreeSum.Structured.Indexed.integerInverse_correct line 192
  23. def OAI.DeterministicThreeSum.Structured.Indexed.scaledTable line 221
  24. def OAI.DeterministicThreeSum.Structured.Indexed.scaledMemory line 227
  25. theorem OAI.DeterministicThreeSum.Structured.Indexed.scaledTable_correct line 232
  26. lemma OAI.DeterministicThreeSum.Structured.Indexed.scaledMemory_outside line 269
  27. lemma OAI.DeterministicThreeSum.Structured.Indexed.scaledMemory_entry line 277
  28. lemma OAI.DeterministicThreeSum.Structured.Indexed.scaled_cast line 291
  29. def OAI.DeterministicThreeSum.Structured.Indexed.commonTable line 298
  30. theorem OAI.DeterministicThreeSum.Structured.Indexed.commonTable_correct line 302