OAI/Algebra/OddKaplansky/Gluing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OddKaplansky.Gluing.con line 16
2. def OAI.OddKaplansky.Gluing.Q line 20
3. instance OAI.OddKaplansky.Gluing.(instance at line 21) line 21
4. def OAI.OddKaplansky.Gluing.vertex line 23
5. lemma OAI.OddKaplansky.Gluing.edge_eq line 25
6. def OAI.OddKaplansky.Gluing.lift line 29
7. lemma OAI.OddKaplansky.Gluing.lift_vertex line 35
8. theorem OAI.OddKaplansky.Gluing.vertex_injective line 41
9. instance OAI.OddKaplansky.Gluing.(instance at line 63) line 63