OAI/Combinatorics/VariableWL/Coordinates.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VariableWL.BlockCoordinates.Coordinate line 12
  2. instance OAI.VariableWL.BlockCoordinates.coordinateFintype line 17
  3. def OAI.VariableWL.BlockCoordinates.coordinateEquiv line 20
  4. def OAI.VariableWL.BlockCoordinates.numbering line 42
  5. def OAI.VariableWL.BlockCoordinates.encode line 45
  6. def OAI.VariableWL.BlockCoordinates.readoutDimension line 52
  7. def OAI.VariableWL.BlockCoordinates.readoutEquiv line 56
  8. theorem OAI.VariableWL.BlockCoordinates.coordinate_lift line 67
  9. def OAI.VariableWL.BlockCoordinates.readoutEmbedding line 97
  10. theorem OAI.VariableWL.BlockCoordinates.readoutEmbedding_spec line 102
  11. theorem OAI.VariableWL.BlockCoordinates.readoutDimension_le line 109
  12. theorem OAI.VariableWL.BlockCoordinates.exists_readout_order line 114
  13. abbrev OAI.VariableWL.BlockCoordinates.Proper line 132
  14. instance OAI.VariableWL.BlockCoordinates.(instance at line 135) line 135
  15. def OAI.VariableWL.BlockCoordinates.properNumber line 140
  16. def OAI.VariableWL.BlockCoordinates.channelRoot line 147
  17. def OAI.VariableWL.BlockCoordinates.channelOrder line 151
  18. def OAI.VariableWL.BlockCoordinates.data line 156
  19. def OAI.VariableWL.BlockCoordinates.valuationEquiv line 179
  20. def OAI.VariableWL.BlockCoordinates.properSwap line 189
  21. def OAI.VariableWL.BlockCoordinates.channelEquiv line 195
  22. theorem OAI.VariableWL.BlockCoordinates.channelRoot_number line 206
  23. def OAI.VariableWL.BlockCoordinates.wiring line 212
  24. theorem OAI.VariableWL.BlockCoordinates.readout_prefix line 247
  25. theorem OAI.VariableWL.BlockCoordinates.channelOrder_number line 265
  26. theorem OAI.VariableWL.BlockCoordinates.data_prefix line 273
  27. theorem OAI.VariableWL.BlockCoordinates.mate_channel line 284
  28. def OAI.VariableWL.BlockCoordinates.encodeList line 292
  29. theorem OAI.VariableWL.BlockCoordinates.rootShift_encode line 296
  30. theorem OAI.VariableWL.BlockCoordinates.compatible_of_agree line 302
  31. theorem OAI.VariableWL.PrefixParts.Wiring.uncoloredTranslation_local line 325