OAI/Combinatorics/VariableWL/Wrapping.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VariableWL.Wrapping.Bit line 10
  2. structure OAI.VariableWL.Wrapping.RowDiagram line 14
  3. def OAI.VariableWL.Wrapping.RowDiagram.rowWeight line 28
  4. def OAI.VariableWL.Wrapping.RowDiagram.Wraps line 30
  5. theorem OAI.VariableWL.Wrapping.RowDiagram.boundary_incidence line 33
  6. theorem OAI.VariableWL.Wrapping.RowDiagram.row_parity_next line 48
  7. theorem OAI.VariableWL.Wrapping.RowDiagram.row_parity_all line 59
  8. theorem OAI.VariableWL.Wrapping.RowDiagram.finRotate_orbit line 70
  9. theorem OAI.VariableWL.Wrapping.RowDiagram.covers_rows line 76
  10. theorem OAI.VariableWL.Wrapping.RowDiagram.blocks_card_ge line 92
  11. theorem OAI.VariableWL.Wrapping.RowDiagram.row_injective line 103
  12. def OAI.VariableWL.Wrapping.RowDiagram.Labeled line 124
  13. theorem OAI.VariableWL.Wrapping.RowDiagram.label_incidence line 134
  14. theorem OAI.VariableWL.Wrapping.RowDiagram.label_coherence line 154
  15. theorem OAI.VariableWL.Wrapping.overlap_compl_card_le_one line 178
  16. theorem OAI.VariableWL.Wrapping.adjacent_cover line 191
  17. theorem OAI.VariableWL.Wrapping.overlap_address_unique line 209
  18. theorem OAI.VariableWL.Wrapping.finRotate_no_fixed line 225