OAI/Combinatorics/SumProduct/Alignment/RationalLattice15.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalLattice.WeightedLawChart.law line 27
  2. def OAI.RationalLattice.WeightedLawChart.difference line 29
  3. lemma OAI.RationalLattice.WeightedLawChart.difference_left line 33
  4. lemma OAI.RationalLattice.WeightedLawChart.difference_right line 39
  5. def OAI.RationalLattice.WeightedLawChart.extend line 45
  6. def OAI.RationalLattice.WeightedLawChart.restrict line 50
  7. lemma OAI.RationalLattice.WeightedLawChart.extend_polynomial line 55
  8. lemma OAI.RationalLattice.WeightedLawChart.difference_polynomial line 75
  9. lemma OAI.RationalLattice.WeightedLawChart.difference_restrict line 81
  10. lemma OAI.RationalLattice.WeightedLawChart.exists_correction line 111
  11. def OAI.RationalLattice.WeightedLawChart.realCoordinates line 118
  12. def OAI.RationalLattice.PolynomialArrays.IsArray line 150
  13. lemma OAI.RationalLattice.PolynomialArrays.one_array line 154
  14. lemma OAI.RationalLattice.PolynomialArrays.mul_array line 159
  15. lemma OAI.RationalLattice.PolynomialArrays.log_inv line 172
  16. lemma OAI.RationalLattice.PolynomialArrays.inv_array line 178
  17. def OAI.RationalLattice.PolynomialArrays.group line 186
  18. lemma OAI.RationalLattice.PolynomialArrays.constant line 193
  19. lemma OAI.RationalLattice.PolynomialArrays.affine_weighted line 196
  20. lemma OAI.RationalLattice.PolynomialArrays.power_affine line 204
  21. lemma OAI.RationalLattice.PolynomialArrays.source_array line 213
  22. lemma OAI.RationalLattice.PolynomialArrays.translate_array line 218
  23. def OAI.RationalLattice.PolynomialArrays.shift line 225
  24. lemma OAI.RationalLattice.PolynomialArrays.shift_continuous line 235
  25. def OAI.RationalLattice.PolynomialArrays.lattice line 240
  26. lemma OAI.RationalLattice.PolynomialArrays.shift_lattice line 246