OAI/Combinatorics/Ryser/Construction/CosetIndex.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Construction.embeddedUnits line 14
  2. theorem OAI.RyserCoveringCounterexample.Construction.embeddedUnits_injective line 16
  3. def OAI.RyserCoveringCounterexample.Construction.smallUnitSubgroup line 19
  4. abbrev OAI.RyserCoveringCounterexample.Construction.CosetIndex line 21
  5. def OAI.RyserCoveringCounterexample.Construction.unitCoset line 23
  6. def OAI.RyserCoveringCounterexample.Construction.cosetRepresentative line 25
  7. theorem OAI.RyserCoveringCounterexample.Construction.cosetRepresentative_one line 29
  8. theorem OAI.RyserCoveringCounterexample.Construction.unitCoset_representative line 34
  9. theorem OAI.RyserCoveringCounterexample.Construction.cosetRepresentative_injective line 43
  10. theorem OAI.RyserCoveringCounterexample.Construction.unitCoset_eq_iff line 49
  11. theorem OAI.RyserCoveringCounterexample.Construction.unitCoset_eq_one_iff line 56
  12. theorem OAI.RyserCoveringCounterexample.Construction.exists_embeddedUnit_mul_representative line 62
  13. abbrev OAI.RyserCoveringCounterexample.Construction.ConfigurationGroup line 70
  14. def OAI.RyserCoveringCounterexample.Construction.identityGroup line 72
  15. def OAI.RyserCoveringCounterexample.Construction.extraGroup line 74
  16. theorem OAI.RyserCoveringCounterexample.Construction.natCard_smallUnitSubgroup line 76
  17. theorem OAI.RyserCoveringCounterexample.Construction.natCard_cosetIndex_mul line 83
  18. instance OAI.RyserCoveringCounterexample.Construction.(instance at line 93) line 93
  19. theorem OAI.RyserCoveringCounterexample.Construction.card_cosetIndex_mul line 95
  20. theorem OAI.RyserCoveringCounterexample.Construction.card_configurationGroup line 99