OAI/Combinatorics/Ryser/Construction/GroupPlacement.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.embeddedDirections line 13
  2. def OAI.RyserCoveringCounterexample.Construction.groupPlacement line 16
  3. def OAI.RyserCoveringCounterexample.Construction.groupAltered line 21
  4. def OAI.RyserCoveringCounterexample.Construction.groupAxes line 25
  5. def OAI.RyserCoveringCounterexample.Construction.groupConflict line 29
  6. theorem OAI.RyserCoveringCounterexample.Construction.groupAltered_card line 36
  7. theorem OAI.RyserCoveringCounterexample.Construction.groupAxes_card line 41
  8. theorem OAI.RyserCoveringCounterexample.Construction.embeddedDirections_card line 45
  9. theorem OAI.RyserCoveringCounterexample.Construction.coset_altered_embedded_index line 50
  10. theorem OAI.RyserCoveringCounterexample.Construction.identity_altered_subset_embedded line 71
  11. theorem OAI.RyserCoveringCounterexample.Construction.groupAltered_subset_conflict line 78
  12. theorem OAI.RyserCoveringCounterexample.Construction.exists_groupAltered line 97
  13. theorem OAI.RyserCoveringCounterexample.Construction.shared_groupConflict line 109
  14. theorem OAI.RyserCoveringCounterexample.Construction.shared_groupAltered line 154
  15. theorem OAI.RyserCoveringCounterexample.Construction.groupConflict_multiplicity_le_two line 167
  16. theorem OAI.RyserCoveringCounterexample.Construction.groupAltered_multiplicity_le_two line 191