OAI/Combinatorics/SumProduct/Alignment/RationalQuotient01.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalLattice.integerCoordinates_rational line 26
  2. lemma OAI.RationalLattice.integerCoordinates_discrete line 32
  3. def OAI.RationalLattice.coordinateTail line 75
  4. lemma OAI.RationalLattice.mem_coordinateTail line 88
  5. lemma OAI.RationalLattice.coordinateTail_zero line 90
  6. lemma OAI.RationalLattice.coordinateTail_end line 93
  7. lemma OAI.RationalLattice.coordinateTail_antitone line 101
  8. lemma OAI.RationalLattice.coordinateTail_normal line 105
  9. lemma OAI.RationalLattice.coordinateTail_commutator line 115
  10. theorem OAI.RationalLattice.nilpotent_of_coordinates line 134
  11. theorem OAI.RationalLattice.coordinateTail_compact_reps line 146
  12. def OAI.RationalQuotientFunctions.cosetLift line 187
  13. lemma OAI.RationalQuotientFunctions.cosetLift_mk line 194
  14. lemma OAI.RationalQuotientFunctions.continuous_cosetLift line 200
  15. lemma OAI.RationalQuotientFunctions.normal_lift_invariant line 210
  16. def OAI.RationalQuotientFunctions.normalDescend line 221
  17. lemma OAI.RationalQuotientFunctions.normalDescend_mk line 228
  18. lemma OAI.RationalQuotientFunctions.continuous_normalDescend line 234
  19. lemma OAI.RationalQuotientFunctions.normalDescend_forall line 243
  20. theorem OAI.RationalQuotientFunctions.existsUnique_normalDescend line 256
  21. def OAI.RationalQuotientFunctions.quotientMap line 270
  22. lemma OAI.RationalQuotientFunctions.continuous_quotientMap line 276
  23. lemma OAI.RationalQuotientFunctions.quotientMap_surjective line 281