OAI/Combinatorics/Ryser/Construction/GadgetAlgebra.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.cubeMap line 17
  2. def OAI.RyserCoveringCounterexample.Construction.cubicPoint line 19
  3. theorem OAI.RyserCoveringCounterexample.Construction.cubicPoint_injective line 21
  4. theorem OAI.RyserCoveringCounterexample.Construction.cube_bijective line 28
  5. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_bijective line 46
  6. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_vertical_iff line 58
  7. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_horizontal_iff line 68
  8. def OAI.RyserCoveringCounterexample.Construction.cubicShape line 75
  9. theorem OAI.RyserCoveringCounterexample.Construction.mem_cubicShape line 78
  10. theorem OAI.RyserCoveringCounterexample.Construction.cubicShape_card line 82
  11. theorem OAI.RyserCoveringCounterexample.Construction.cubicShape_eq_image_linePoints line 87
  12. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_image_vertical line 106
  13. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_image_horizontal line 120
  14. def OAI.RyserCoveringCounterexample.Construction.cubicLinePolynomial line 136
  15. theorem OAI.RyserCoveringCounterexample.Construction.eval_cubicLinePolynomial_eq_zero_iff line 140
  16. theorem OAI.RyserCoveringCounterexample.Construction.cubicLinePolynomial_ne_zero line 146
  17. theorem OAI.RyserCoveringCounterexample.Construction.cubicLinePolynomial_natDegree_le line 160
  18. theorem OAI.RyserCoveringCounterexample.Construction.cubicShape_filter_incidence_card_le line 172
  19. theorem OAI.RyserCoveringCounterexample.Construction.cubicShape_inter_linePoints_card_le line 185
  20. theorem OAI.RyserCoveringCounterexample.Construction.cubicShape_ne_linePoints line 195
  21. theorem OAI.RyserCoveringCounterexample.Construction.cubicShape_injective line 207
  22. theorem OAI.RyserCoveringCounterexample.Construction.cubicShape_intercept_unique line 228
  23. theorem OAI.RyserCoveringCounterexample.Construction.cubicShape_intercept_card line 245
  24. theorem OAI.RyserCoveringCounterexample.Construction.coprime_three_zmod_card_sub_one line 255
  25. theorem OAI.RyserCoveringCounterexample.Construction.cube_bijective_zmod line 263
  26. theorem OAI.RyserCoveringCounterexample.Construction.cubeMap_bijective_zmod line 267