OAI/Topology/ArtinGroups/ParabolicIntersections/AmalgamGraph.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The coset graph of a two-factor amalgam, with its genuine group action.

  1. abbrev OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.Amalgam line 15
  2. abbrev OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.Factor line 16
  3. abbrev OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.Vertex line 17
  4. def OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.vertex line 19
  5. def OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.graph line 21
  6. instance OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.(instance at line 28) line 28
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.smul_vertex line 39
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.vertex_adj line 42
  9. def OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.translate line 45
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.vertex_factor_fixed line 55
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.root_to_base line 63
  12. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.base_to_base line 69
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.root_to_vertex line 73
  14. theorem OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.connected line 98
  15. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.vertex_stabilizer line 106
  16. lemma OAI.HarmonicArtin.ParabolicIntersections.AmalgamTree.edge_stabilizer line 118