OAI/Analysis/PeriodicLattice/RationalArithmetic.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Uniform lattice constants and computable reduced rational arithmetic.

  1. theorem OAI.PeriodicLattice.RecursiveArithmetic.program_of_computable line 16
  2. def OAI.PeriodicLattice.Quantitative.latticeConstants line 27
  3. theorem OAI.PeriodicLattice.Quantitative.latticeConstants_effective line 32
  4. theorem OAI.PeriodicLattice.Quantitative.latticeConstants_bounds line 41
  5. theorem OAI.PeriodicLattice.RecursiveArithmetic.natDvd line 63
  6. def OAI.PeriodicLattice.RecursiveArithmetic.gcdSearch line 67
  7. theorem OAI.PeriodicLattice.RecursiveArithmetic.gcdSearch_eq line 70
  8. theorem OAI.PeriodicLattice.RecursiveArithmetic.nat_gcd line 88
  9. theorem OAI.PeriodicLattice.RecursiveArithmetic.natCoprime line 94
  10. theorem OAI.PeriodicLattice.RecursiveArithmetic.reducedPred line 97
  11. abbrev OAI.PeriodicLattice.RecursiveArithmetic.ReducedPair line 101
  12. def OAI.PeriodicLattice.RecursiveArithmetic.ratEquiv line 104
  13. def OAI.PeriodicLattice.RecursiveArithmetic.rationalPrimcodable line 110
  14. theorem OAI.PeriodicLattice.RecursiveArithmetic.encodable_ext line 112
  15. theorem OAI.PeriodicLattice.RecursiveArithmetic.rational_encoding line 120
  16. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratEncoding line 140
  17. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratNum line 142
  18. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratDen line 146
  19. theorem OAI.PeriodicLattice.RecursiveArithmetic.int_div line 150
  20. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratMk line 189
  21. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratInt line 203
  22. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratNat line 208
  23. theorem OAI.PeriodicLattice.RecursiveArithmetic.rat_add line 211
  24. theorem OAI.PeriodicLattice.RecursiveArithmetic.rat_mul line 218
  25. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratNeg line 224
  26. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratDivInt line 229
  27. theorem OAI.PeriodicLattice.RecursiveArithmetic.ratInv line 237
  28. theorem OAI.PeriodicLattice.RecursiveArithmetic.rat_sub line 240
  29. theorem OAI.PeriodicLattice.RecursiveArithmetic.rat_div line 243
  30. theorem OAI.PeriodicLattice.RecursiveArithmetic.rat_pow line 246