OAI/Combinatorics/SumProduct/Alignment/RationalLattice05.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalLattice.IsPolynomialMap line 18
  2. lemma OAI.RationalLattice.polynomialMap_const line 21
  3. lemma OAI.RationalLattice.polynomialMap_one line 27
  4. lemma OAI.RationalLattice.polynomialMap_mul line 30
  5. lemma OAI.RationalLattice.polynomialMap_basisFlow line 43
  6. lemma OAI.RationalLattice.polynomialMap_peel line 55
  7. lemma OAI.RationalLattice.polynomial_expCoordinates line 66
  8. lemma OAI.RationalLattice.polynomialMap_expProduct line 69
  9. lemma OAI.MalcevCharacters.coord_axis line 95
  10. lemma OAI.MalcevCharacters.axis_zero line 99
  11. lemma OAI.MalcevCharacters.axis_continuous line 105
  12. def OAI.MalcevCharacters.axisCharacter line 120
  13. lemma OAI.MalcevCharacters.axisCharacter_continuous line 129
  14. lemma OAI.MalcevCharacters.character_axis line 133
  15. theorem OAI.MalcevCharacters.character_coordinates line 142
  16. lemma OAI.MalcevCharacters.axis_one_mem line 158
  17. theorem OAI.MalcevCharacters.integer_character_coordinates line 170
  18. def OAI.MalcevCharacters.coordinateForm line 179
  19. lemma OAI.MalcevCharacters.kernel_eq_image line 185
  20. theorem OAI.MalcevCharacters.kernel_connected line 206
  21. def OAI.RationalLattice.prefixProduct line 224
  22. lemma OAI.RationalLattice.prefix_mul_tail line 227
  23. lemma OAI.RationalLattice.expProduct_coord line 231
  24. lemma OAI.RationalLattice.prefixProduct_eq line 237
  25. lemma OAI.RationalLattice.expProduct_coord_sub line 249
  26. lemma OAI.RationalLattice.expProduct_coord_eq line 255
  27. lemma OAI.RationalLattice.expCoordinates_prefix_eq line 262
  28. lemma OAI.RationalLattice.expCoordinates_coord_sub line 282
  29. def OAI.RationalLattice.lowerExtend line 292
  30. lemma OAI.RationalLattice.expCoordinates_mul_difference line 295
  31. lemma OAI.RationalLattice.exists_second_correction line 341
  32. lemma OAI.RationalLattice.expProduct_zero line 356
  33. lemma OAI.RationalLattice.expCoordinates_one line 363
  34. def OAI.RationalLattice.secondCorrection line 366
  35. lemma OAI.RationalLattice.second_mul_coord line 369
  36. def OAI.RationalLattice.secondCoordinates line 383
  37. lemma OAI.RationalLattice.expProduct_single line 389
  38. lemma OAI.RationalLattice.second_axis line 397
  39. theorem OAI.RationalLattice.secondCoordinates_secondKind line 402
  40. lemma OAI.RationalLattice.coordinates_prefix_zeros_iff line 409
  41. theorem OAI.RationalLattice.secondCoordinates_adapted line 430