OAI/Combinatorics/SumProduct/Alignment/LeibmanSquare02.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LeibmanSquare.first_eq_pairTail line 28
  2. def OAI.LeibmanSquare.firstPairEquiv line 34
  3. lemma OAI.LeibmanSquare.firstPairEquiv_val line 38
  4. lemma OAI.LeibmanSquare.firstPairEquiv_continuous line 42
  5. lemma OAI.LeibmanSquare.firstPairEquiv_symm_continuous line 45
  6. lemma OAI.LeibmanSquare.restricted_map_pairLevel line 49
  7. lemma OAI.LeibmanSquare.last_map_diagonal line 69
  8. lemma OAI.LeibmanSquare.last_central_ambient line 87
  9. def OAI.LeibmanSquare.reducedPairEquiv line 101
  10. lemma OAI.LeibmanSquare.reducedPairEquiv_mk line 107
  11. lemma OAI.LeibmanSquare.reducedPairEquiv_continuous line 112
  12. lemma OAI.LeibmanSquare.reducedPairEquiv_symm_continuous line 118
  13. def OAI.LeibmanSquare.reducedPairHomeomorph line 123
  14. def OAI.RationalLattice.pullCoordinates line 141
  15. lemma OAI.LeibmanSquare.squareLattice_map line 162
  16. lemma OAI.LeibmanSquare.reducedLattice_map line 173
  17. lemma OAI.LeibmanSquare.reducedLevel_map line 187
  18. def OAI.LeibmanSquare.sourceReducedCoordinates line 207
  19. lemma OAI.LeibmanSquare.sourceReduced_integer_lattice line 215
  20. def OAI.MalcevSubspaceQuotient.mask line 249
  21. def OAI.MalcevSubspaceQuotient.strip line 253
  22. lemma OAI.MalcevSubspaceQuotient.axis_mem line 257
  23. lemma OAI.MalcevSubspaceQuotient.mk_coordinates line 265
  24. lemma OAI.MalcevSubspaceQuotient.mk_strip line 276
  25. lemma OAI.MalcevSubspaceQuotient.strip_unique line 289
  26. theorem OAI.MalcevSubspaceQuotient.eq_coset_iff line 315