OAI/Combinatorics/SumProduct/Alignment/RationalLattice04.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RationalLattice.powerPolynomial_rational line 17
  2. theorem OAI.RationalLattice.realPower_rational line 33
  3. lemma OAI.RationalLattice.coord_mul_of_left_zero line 54
  4. lemma OAI.RationalLattice.coord_mul_of_right_zero line 70
  5. lemma OAI.RationalLattice.realPower_coord_of_lower_zero line 86
  6. def OAI.RationalLattice.basisElement line 100
  7. def OAI.RationalLattice.basisFlow line 101
  8. lemma OAI.RationalLattice.basisFlow_continuous line 103
  9. lemma OAI.RationalLattice.basisFlow_zero line 105
  10. lemma OAI.RationalLattice.basisFlow_add line 106
  11. lemma OAI.RationalLattice.basisFlow_neg line 108
  12. lemma OAI.RationalLattice.basisFlow_coord line 111
  13. def OAI.RationalLattice.peel line 123
  14. lemma OAI.RationalLattice.peel_continuous line 129
  15. lemma OAI.RationalLattice.peel_zero_coordinates line 139
  16. lemma OAI.RationalLattice.peel_dimension line 161
  17. def OAI.RationalLattice.expCoordinates line 166
  18. def OAI.RationalLattice.tailProduct line 168
  19. def OAI.RationalLattice.expProduct line 171
  20. lemma OAI.RationalLattice.tailProduct_dimension line 173
  21. lemma OAI.RationalLattice.tailProduct_step line 178
  22. lemma OAI.RationalLattice.tailProduct_lower line 183
  23. lemma OAI.RationalLattice.tailProduct_coord line 196
  24. lemma OAI.RationalLattice.peel_expProduct line 204
  25. lemma OAI.RationalLattice.expCoordinates_expProduct line 214
  26. lemma OAI.RationalLattice.tailProduct_expCoordinates line 218
  27. lemma OAI.RationalLattice.expProduct_expCoordinates line 226
  28. lemma OAI.RationalLattice.expCoordinates_continuous line 229
  29. lemma OAI.RationalLattice.expProduct_continuous line 234
  30. def OAI.RationalLattice.secondKindHomeomorph line 241
  31. lemma OAI.MalcevPrefixQuotient.prefix_eq_iff line 265
  32. lemma OAI.MalcevPrefixQuotient.eq_coset_iff line 292
  33. def OAI.MalcevPrefixQuotient.embed line 298
  34. def OAI.MalcevPrefixQuotient.lift line 299
  35. lemma OAI.MalcevPrefixQuotient.lift_embed line 300
  36. lemma OAI.MalcevPrefixQuotient.lift_continuous line 302
  37. def OAI.MalcevPrefixQuotient.coordinates line 310
  38. lemma OAI.MalcevPrefixQuotient.coordinates_mk line 315
  39. def OAI.MalcevPrefixQuotient.represent line 318
  40. def OAI.MalcevPrefixQuotient.rebuild line 319
  41. lemma OAI.MalcevPrefixQuotient.coordinates_rebuild line 321
  42. lemma OAI.MalcevPrefixQuotient.rebuild_coordinates line 324
  43. lemma OAI.MalcevPrefixQuotient.coordinates_continuous line 329
  44. lemma OAI.MalcevPrefixQuotient.rebuild_continuous line 335
  45. def OAI.MalcevPrefixQuotient.homeomorph line 338
  46. def OAI.MalcevPrefixQuotient.quotientChart line 350