OAI/Topology/ArtinGroups/ParabolicIntersections/MeshQuiver.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The simple graph of a finite induced reversible quiver.

  1. def OAI.HarmonicArtin.ParabolicIntersections.QuiverSimpleOn line 12
  2. def OAI.HarmonicArtin.ParabolicIntersections.meshQuiverGraph line 15
  3. def OAI.HarmonicArtin.ParabolicIntersections.meshChosenArrow line 26
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.meshChosenArrow_source line 29
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.meshChosenArrow_target line 32
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.meshChosenArrow_eq line 35
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.meshChosenArrow_reverse line 43
  8. def OAI.HarmonicArtin.ParabolicIntersections.meshQuiverNeighborEquiv line 50