OAI/Combinatorics/SumProduct/Alignment/RationalLattice08.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalCharacterFirst.coordinates line 29
  2. lemma OAI.RationalCharacterFirst.exists_correction line 31
  3. def OAI.RationalCharacterFirst.tailCorrection line 59
  4. lemma OAI.RationalCharacterFirst.tail_mul_coord line 63
  5. lemma OAI.RationalCharacterFirst.head_mul_coord line 95
  6. def OAI.RationalCharacterFirst.characterFirstCoordinates line 103
  7. lemma OAI.RationalCharacterFirst.inclusion_polynomial line 119
  8. lemma OAI.RationalCharacterFirst.characterFirst_adapted line 127
  9. theorem OAI.TriangularDenominators.polynomial_origin_grid line 169
  10. theorem OAI.TriangularDenominators.polynomial_origin_grid_real line 206
  11. def OAI.RationalLattice.correctionDenom line 244
  12. lemma OAI.RationalLattice.correctionDenom_pos line 247
  13. lemma OAI.RationalLattice.correction_at_zero line 250
  14. def OAI.RationalLattice.OnGrid line 262
  15. lemma OAI.RationalLattice.correction_on_grid line 265
  16. lemma OAI.RationalLattice.onGrid_mul line 292
  17. lemma OAI.RationalLattice.onGrid_inv line 303
  18. def OAI.RationalLattice.weightedLattice line 324
  19. theorem OAI.RationalLattice.exists_lattice_weights line 332
  20. def OAI.RationalLattice.divideCoordinates line 351
  21. lemma OAI.RationalLattice.exists_scaled_correction line 359
  22. def OAI.RationalLattice.scaledCorrection line 377
  23. def OAI.RationalLattice.scaledCoordinates line 381
  24. lemma OAI.RationalLattice.weightedLattice_iff line 397