OAI/Combinatorics/SumProduct/Alignment/RationalLattice16.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalPolynomialMap.finset_sum line 23
  2. def OAI.RationalLattice.PolynomialArrays.weight line 40
  3. lemma OAI.RationalLattice.PolynomialArrays.toLog_weighted line 42
  4. lemma OAI.RationalLattice.PolynomialArrays.toLog_integer_polynomial line 52
  5. def OAI.RationalLattice.PolynomialArrays.multiply line 64
  6. lemma OAI.RationalLattice.PolynomialArrays.multiply_polynomial line 70
  7. lemma OAI.RationalLattice.PolynomialArrays.multiply_weighted line 88
  8. lemma OAI.RationalLattice.PolynomialArrays.coefficientHomeomorph_mul line 104
  9. def OAI.RationalLattice.FiniteWeightedLawChart.reindex line 132
  10. lemma OAI.RationalLattice.FiniteWeightedLawChart.reindex_one line 141
  11. def OAI.RationalLattice.FiniteWeightedLawChart.law line 143
  12. def OAI.RationalLattice.FiniteWeightedLawChart.reshuffle line 146
  13. lemma OAI.RationalLattice.FiniteWeightedLawChart.law_reindex line 150
  14. lemma OAI.RationalLattice.FiniteWeightedLawChart.reshuffle_polynomial line 154
  15. lemma OAI.RationalLattice.FiniteWeightedLawChart.reshuffle_weighted line 160
  16. def OAI.RationalLattice.FiniteWeightedLawChart.chart line 178
  17. lemma OAI.RationalLattice.FiniteWeightedLawChart.chart_apply line 187
  18. lemma OAI.RationalLattice.FiniteWeightedLawChart.chart_symm_apply line 189
  19. lemma OAI.RationalLattice.PolynomialArrays.finite_law_eq line 213
  20. def OAI.RationalLattice.PolynomialArrays.chart line 221
  21. def OAI.RationalLattice.PolynomialArrays.orderedWeight line 227
  22. lemma OAI.RationalLattice.PolynomialArrays.orderedWeight_pos line 230
  23. lemma OAI.RationalLattice.PolynomialArrays.orderedWeight_monotone line 231
  24. def OAI.RationalLattice.PolynomialArrays.level line 234
  25. def OAI.RationalLattice.PolynomialArrays.filtration line 240
  26. lemma OAI.RationalLattice.PolynomialArrays.coefficients_adapted line 248
  27. lemma OAI.RationalLattice.PolynomialArrays.chart_adapted line 270
  28. def OAI.RationalLattice.PolynomialArrays.secondChart line 280
  29. lemma OAI.RationalLattice.PolynomialArrays.secondChart_secondKind line 282
  30. lemma OAI.RationalLattice.PolynomialArrays.secondChart_adapted line 285