OAI/Geometry/HyperbolicGroups/Occurrence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Shape line 20

   Source documentation

   Table types and the incidence of all seven fan slots of every top. Fans are indexed once, including those used by more than one top.

   abbrev Shape (s u q : ℕ) := Σ t : Fin u → Fin 7,
   …

2. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.Entry line 23
3. def OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.probability line 25
4. lemma OAI.HyperbolicObstruction.IncidenceTemplate.Occurrences.probability_mem line 29