OAI/Algebra/OddKaplansky/SourceGluing.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OddKaplansky.SourceGluing.pDefinition line 12
  2. opaque OAI.OddKaplansky.SourceGluing.pWrapped line 13
  3. def OAI.OddKaplansky.SourceGluing.p line 15
  4. theorem OAI.OddKaplansky.SourceGluing.p_def line 16
  5. lemma OAI.OddKaplansky.SourceGluing.p_prime line 22
  6. lemma OAI.OddKaplansky.SourceGluing.p_gt line 23
  7. instance OAI.OddKaplansky.SourceGluing.(instance at line 25) line 25
  8. instance OAI.OddKaplansky.SourceGluing.(instance at line 26) line 26
  9. def OAI.OddKaplansky.SourceGluing.modulus line 27
  10. lemma OAI.OddKaplansky.SourceGluing.modulus_gt line 28
  11. instance OAI.OddKaplansky.SourceGluing.(instance at line 33) line 33
  12. abbrev OAI.OddKaplansky.SourceGluing.H line 34
  13. def OAI.OddKaplansky.SourceGluing.edgeHom line 36
  14. lemma OAI.OddKaplansky.SourceGluing.neighbor_cast_injective line 39
  15. lemma OAI.OddKaplansky.SourceGluing.shortWords line 49
  16. abbrev OAI.OddKaplansky.SourceGluing.Gā‚€ line 66
  17. def OAI.OddKaplansky.SourceGluing.vertex line 67
  18. lemma OAI.OddKaplansky.SourceGluing.vertex_injective line 68
  19. instance OAI.OddKaplansky.SourceGluing.(instance at line 71) line 71