OAI/Combinatorics/SumProduct/Alignment/RationalTail02.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalTailCoordinates.extendCoefficient line 28
  2. lemma OAI.RationalTailCoordinates.sum_extend line 32
  3. lemma OAI.RationalTailCoordinates.sum_extend_int line 40
  4. theorem OAI.RationalTailCoordinates.exists_integer_extension line 51
  5. theorem OAI.RationalCharacterFirst.exists_refined_integer_cover line 107
  6. lemma OAI.RationalTailCoordinates.mapped_kernel_eq_inter line 153
  7. theorem OAI.RationalTailCoordinates.exists_lower_refinement_geometry line 174
  8. lemma OAI.MalcevCharacters.prefix_coord_mul line 219
  9. def OAI.MalcevCharacters.horizontalCoordinates line 230
  10. lemma OAI.MalcevCharacters.horizontalCoordinates_correction line 240
  11. lemma OAI.MalcevCharacters.horizontalCoordinates_secondKind line 244
  12. def OAI.RationalLatticeCover.coverMap line 261
  13. lemma OAI.RationalLatticeCover.coverMap_mk line 268
  14. lemma OAI.RationalLatticeCover.coverMap_smul line 272
  15. lemma OAI.RationalLatticeCover.coverMap_surjective line 277
  16. theorem OAI.RationalLatticeCover.map_coordinateHaar line 287