OAI/Algebra/OddKaplansky/GraphEdges.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.GraphEdges.Edge line 12
  2. def OAI.OddKaplansky.GraphEdges.Inc line 13
  3. def OAI.OddKaplansky.GraphEdges.neighbor line 15
  4. lemma OAI.OddKaplansky.GraphEdges.incident_exists line 17
  5. lemma OAI.OddKaplansky.GraphEdges.endpoints_ne line 18
  6. lemma OAI.OddKaplansky.GraphEdges.neighbor_incident line 20
  7. lemma OAI.OddKaplansky.GraphEdges.neighbor_ne line 24
  8. lemma OAI.OddKaplansky.GraphEdges.neighbor_of_other line 27
  9. lemma OAI.OddKaplansky.GraphEdges.endpoints_of_inc line 32
  10. lemma OAI.OddKaplansky.GraphEdges.edge_eq_of_inc line 40
  11. lemma OAI.OddKaplansky.GraphEdges.neighbor_injective line 59
  12. lemma OAI.OddKaplansky.GraphEdges.adj_of_inc line 69
  13. theorem OAI.OddKaplansky.GraphEdges.incidence_girth line 76
  14. structure OAI.OddKaplansky.SourceGraph.Vertex line 106
  15. def OAI.OddKaplansky.SourceGraph.vertexEquiv line 110
  16. instance OAI.OddKaplansky.SourceGraph.(instance at line 116) line 116
  17. instance OAI.OddKaplansky.SourceGraph.(instance at line 117) line 117
  18. lemma OAI.OddKaplansky.SourceGraph.card_vertices line 122
  19. def OAI.OddKaplansky.SourceGraph.index line 128
  20. lemma OAI.OddKaplansky.SourceGraph.index_pos line 131
  21. lemma OAI.OddKaplansky.SourceGraph.index_le line 132
  22. lemma OAI.OddKaplansky.SourceGraph.index_injective line 134
  23. lemma OAI.OddKaplansky.SourceGraph.index_strictMono line 140
  24. def OAI.OddKaplansky.SourceGraph.graph line 144
  25. theorem OAI.OddKaplansky.SourceGraph.no_triangle line 149
  26. abbrev OAI.OddKaplansky.SourceGraph.Edge line 168
  27. abbrev OAI.OddKaplansky.SourceGraph.Inc line 169
  28. abbrev OAI.OddKaplansky.SourceGraph.neighbor line 170
  29. lemma OAI.OddKaplansky.SourceGraph.incidence_girth line 172