OAI/Algebra/GroupRing/ConeBoundaryPaths.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.ConePicture.wordLabel line 14
2. lemma OAI.TorsionFreeZeroDivisors.ConePicture.wordLabel_reverse line 17
3. def OAI.TorsionFreeZeroDivisors.ConePicture.rootPath line 22
4. lemma OAI.TorsionFreeZeroDivisors.ConePicture.rootPath_eval line 27
5. def OAI.TorsionFreeZeroDivisors.ConePicture.trianglePath line 35

   Source documentation

   The actual triangular closed boundary, with a root radial omitted exactly when it is collapsed in the finite CW model. No directed-edge duplication.

   def trianglePath (d : D) : Path (graph Γ R) (R.base (Γ.origin d)) (R.base (Γ.origin d)) :=
   …

   Mentions: OAI.TorsionFreeZeroDivisors.ConePicture.graph

6. lemma OAI.TorsionFreeZeroDivisors.ConePicture.trianglePath_eval line 41
7. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.ConeSpherePicture.reduces_to_empty line 51