OAI/GroupTheory/SimpleAmenable/Simplicial/DiagramResolutionNatural.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RestrictedNerve.diagramHorizontalReindex line 14
2. lemma OAI.RestrictedNerve.diagramTranspose_posReindex line 20
3. lemma OAI.RestrictedNerve.compose_three_squares line 26

   Distinct definitions of this name: OAI/GroupTheory/SimpleAmenable/Simplicial/PositionalInclusionMonoidal.lean:12 (same statement text; different proof or body). Qualify references as OAI.RestrictedNerve.compose_three_squares@path.

4. lemma OAI.RestrictedNerve.diagramResolutionHomologyIso_natural line 39
5. instance OAI.RestrictedNerve.posReindexMonoidal line 71
6. instance OAI.RestrictedNerve.posReindexBraided line 107
7. def OAI.RestrictedNerve.widePosReindex line 112
8. instance OAI.RestrictedNerve.widePosReindexMonoidal line 118
9. instance OAI.RestrictedNerve.widePosReindexBraided line 156