OAI/Combinatorics/SumProduct/Alignment/PairTail01.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MalcevPrefixQuotient.represent_coordinates line 27
  2. lemma OAI.MalcevPrefixQuotient.quotient_coordinates_mk line 32
  3. theorem OAI.MalcevPrefixQuotient.quotient_lattice line 37
  4. theorem OAI.MalcevPrefixQuotient.quotient_adapted line 54
  5. theorem OAI.MalcevPrefixQuotient.quotient_rational line 72
  6. def OAI.PairTail.square line 98
  7. def OAI.PairTail.first line 110
  8. def OAI.PairTail.difference line 112
  9. def OAI.PairTail.pair line 114
  10. lemma OAI.PairTail.first_pair line 117
  11. lemma OAI.PairTail.difference_pair line 119
  12. lemma OAI.PairTail.pair_first_difference line 123
  13. lemma OAI.PairTail.first_continuous line 127
  14. lemma OAI.PairTail.difference_continuous line 128
  15. lemma OAI.PairTail.pair_continuous line 132
  16. def OAI.PairTail.squareHomeomorph line 136
  17. def OAI.PairTail.diagonal line 146
  18. lemma OAI.PairTail.diagonal_normal line 159
  19. lemma OAI.PairTail.eq_coset_iff line 172
  20. def OAI.PairTail.quotientCoordinates line 206
  21. lemma OAI.PairTail.quotientCoordinates_mk line 214
  22. lemma OAI.PairTail.quotientCoordinates_continuous line 217
  23. def OAI.PairTail.quotientRebuild line 223
  24. lemma OAI.PairTail.quotientCoordinates_rebuild line 227
  25. lemma OAI.PairTail.quotientRebuild_coordinates line 232
  26. lemma OAI.PairTail.quotientRebuild_continuous line 238
  27. def OAI.PairTail.quotientHomeomorph line 242
  28. def OAI.RationalPolynomialMap.IsPolynomial line 262
  29. lemma OAI.RationalPolynomialMap.const line 265
  30. lemma OAI.RationalPolynomialMap.zero line 266
  31. lemma OAI.RationalPolynomialMap.one line 267
  32. lemma OAI.RationalPolynomialMap.coordinate line 268
  33. lemma OAI.RationalPolynomialMap.add line 269
  34. lemma OAI.RationalPolynomialMap.mul line 274
  35. lemma OAI.RationalPolynomialMap.neg line 279
  36. lemma OAI.RationalPolynomialMap.sub line 282
  37. lemma OAI.RationalPolynomialMap.eval line 285
  38. lemma OAI.RationalPolynomialMap.comp line 293
  39. lemma OAI.RationalPolynomialMap.polynomial_eval line 298