OAI/Combinatorics/Progressions/Lattices/RecoveredLatticeMatrixInvariance.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.recoveredIntegerTransverse line 18
  2. def OAI.Erdos3.recoveredIntegerDeck line 23
  3. theorem OAI.Erdos3.recoveredIntegerTransverse_projection line 28
  4. theorem OAI.Erdos3.recoveredIntegerTransverse_normalized line 33
  5. theorem OAI.Erdos3.recoveredIntegerDeck_reconstruction line 40
  6. theorem OAI.Erdos3.recoveredIntegerTransverse_of_mem line 46
  7. theorem OAI.Erdos3.recoveredIntegerDeck_of_mem line 59
  8. theorem OAI.Erdos3.recoveredIntegerTransverse_add_retained line 73
  9. theorem OAI.Erdos3.recoveredIntegerDeck_add_retained line 80
  10. def OAI.Erdos3.recoveredMixedCoordinates line 90
  11. theorem OAI.Erdos3.recoveredMixedCoordinates_add line 94
  12. theorem OAI.Erdos3.recoveredMixedCoordinates_zsmul line 100
  13. theorem OAI.Erdos3.recoveredMixedCoordinates_add_retained line 105
  14. theorem OAI.Erdos3.recoveredMixedCoordinates_real line 112
  15. theorem OAI.Erdos3.recoveredMixedCoordinates_point line 129
  16. theorem OAI.Erdos3.recoveredMixedCoordinates_deck line 137
  17. theorem OAI.Erdos3.recoveredIntegerLift_linear_residue line 162
  18. def OAI.Erdos3.layerIntegerRestriction line 175
  19. def OAI.Erdos3.recoveredLayeredIntegerLift line 181
  20. theorem OAI.Erdos3.recoveredIntegerTransverse_layer_matrix line 192
  21. theorem OAI.Erdos3.standardLatticeCoordinates_layer_matrix_residue line 212