OAI/Combinatorics/TriangleRemoval/Spectral/ClosedWalkFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpTerminalLeave.closedWalkFamily line 23
  2. lemma OAI.SharpTerminalLeave.wordOfWalk_adj line 27
  3. def OAI.SharpTerminalLeave.wordOfWalk line 53
  4. lemma OAI.SharpTerminalLeave.wordOfWalk_injective line 60
  5. def OAI.SharpTerminalLeave.walkOfWord line 79
  6. lemma OAI.SharpTerminalLeave.walkOfWord_injective line 89
  7. theorem OAI.SharpTerminalLeave.trace_adjMatrix_eq_closedWords line 99
  8. lemma OAI.SharpTerminalLeave.closedWords_card_eq line 112
  9. theorem OAI.SharpTerminalLeave.link_trace_count_bound line 129