OAI/Algebra/OddKaplansky/LocalGroup.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OddKaplansky.LocalGroup line 10
  2. abbrev OAI.OddKaplansky.LocalGroup.Point line 15
  3. instance OAI.OddKaplansky.LocalGroup.(instance at line 17) line 17
  4. def OAI.OddKaplansky.LocalGroup.u line 20
  5. def OAI.OddKaplansky.LocalGroup.c line 22
  6. def OAI.OddKaplansky.LocalGroup.v line 25
  7. lemma OAI.OddKaplansky.LocalGroup.u_injective line 28
  8. lemma OAI.OddKaplansky.LocalGroup.v_injective line 32
  9. lemma OAI.OddKaplansky.LocalGroup.u_right line 35
  10. lemma OAI.OddKaplansky.LocalGroup.v_right line 37
  11. lemma OAI.OddKaplansky.LocalGroup.v_left_zero line 41
  12. lemma OAI.OddKaplansky.LocalGroup.v_eq_u line 45
  13. def OAI.OddKaplansky.LocalGroup.direction line 59
  14. def OAI.OddKaplansky.LocalGroup.line line 61
  15. lemma OAI.OddKaplansky.LocalGroup.line_injective line 66
  16. def OAI.OddKaplansky.LocalGroup.edgeHom line 71
  17. lemma OAI.OddKaplansky.LocalGroup.edgeHom_injective line 75
  18. lemma OAI.OddKaplansky.LocalGroup.edgeHom_right line 82
  19. lemma OAI.OddKaplansky.LocalGroup.two_directions line 90
  20. lemma OAI.OddKaplansky.LocalGroup.three_directions line 98
  21. lemma OAI.OddKaplansky.LocalGroup.edge_word_one line 109
  22. lemma OAI.OddKaplansky.LocalGroup.edge_word_two line 114
  23. lemma OAI.OddKaplansky.LocalGroup.edge_word_three line 123