OAI/Combinatorics/PolynomialVacuum/Bridge/BridgeWord.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.shiftVertex line 7
  2. def OAI.PolynomialVacuumBridge.Corridor.shiftGerm line 10
  3. theorem OAI.PolynomialVacuumBridge.Corridor.shiftVertex_zero line 11
  4. theorem OAI.PolynomialVacuumBridge.Corridor.shiftGerm_zero line 12
  5. theorem OAI.PolynomialVacuumBridge.Corridor.shiftVertex_add line 13
  6. theorem OAI.PolynomialVacuumBridge.Corridor.shiftGerm_add line 16
  7. theorem OAI.PolynomialVacuumBridge.Corridor.shiftVertex_injective line 18
  8. theorem OAI.PolynomialVacuumBridge.Corridor.layer_shift line 22
  9. theorem OAI.PolynomialVacuumBridge.Corridor.shift_neighbor line 24
  10. theorem OAI.PolynomialVacuumBridge.Corridor.shift_advance line 27
  11. theorem OAI.PolynomialVacuumBridge.Corridor.shift_terminal line 30
  12. theorem OAI.PolynomialVacuumBridge.Corridor.shift_traced line 35
  13. structure OAI.PolynomialVacuumBridge.Corridor.BridgeWord line 43
  14. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.ext line 52
  15. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.one line 58
  16. instance OAI.PolynomialVacuumBridge.Corridor.BridgeWord.(instance at line 59) line 59
  17. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.word_one line 60
  18. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.height_one line 61
  19. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.endX_one line 62
  20. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.word_eq_nil line 63
  21. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.terminal_source line 64
  22. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.positive_of_nonempty line 68
  23. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.mul line 75
  24. instance OAI.PolynomialVacuumBridge.Corridor.BridgeWord.(instance at line 102) line 102
  25. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.word_mul line 103
  26. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.height_mul line 104
  27. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.endX_mul line 105
  28. instance OAI.PolynomialVacuumBridge.Corridor.BridgeWord.(instance at line 106) line 106
  29. theorem OAI.PolynomialVacuumBridge.Corridor.BridgeWord.length_nonzero line 111
  30. def OAI.PolynomialVacuumBridge.Corridor.BridgeWord.IsPrimitive line 113