OAI/GroupTheory/SimpleAmenable/Simplicial/MonoidalCongruence.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IntervalBar.Diagram.monoidal_congr line 13
  2. lemma OAI.IntervalBar.Diagram.map_congr line 31
  3. lemma OAI.RestrictedNerve.transpose_ε line 51
  4. lemma OAI.RestrictedNerve.transpose_μ line 53
  5. lemma OAI.RestrictedNerve.reindex_ε line 56
  6. lemma OAI.RestrictedNerve.map_reindex_ε line 58
  7. lemma OAI.RestrictedNerve.map_reindex_μ line 60
  8. lemma OAI.RestrictedNerve.transpose_reindex line 62

    Distinct definitions of this name: OAI/GroupTheory/SimpleAmenable/Simplicial/RestrictedMonoidalTranspose.lean:274 (different declaration text). Qualify references as OAI.RestrictedNerve.transpose_reindex@path.

  9. abbrev OAI.RestrictedNerve.transposeReindexLeft line 66
  10. abbrev OAI.RestrictedNerve.transposeReindexRight line 67
  11. abbrev OAI.RestrictedNerve.transposeReindexHom line 68
  12. lemma OAI.RestrictedNerve.transpose_comp_app line 70
  13. lemma OAI.RestrictedNerve.transpose_tensor_app line 75
  14. lemma OAI.RestrictedNerve.transpose_reindex_unit line 82
  15. lemma OAI.RestrictedNerve.transposeReindexHom_app line 95
  16. lemma OAI.RestrictedNerve.transposeReindexLeft_μ_app line 103
  17. lemma OAI.RestrictedNerve.transpose_reindex_tensor line 111
  18. instance OAI.RestrictedNerve.transpose_reindex_monoidal line 132
  19. lemma OAI.IntervalBar.Diagram.braided_congr line 147
  20. lemma OAI.IntervalBar.Diagram.map₂_congr line 157
  21. lemma OAI.RestrictedNerve.tripleTranspose_reindex line 177
  22. def OAI.RestrictedNerve.tripleDiagramTranspose line 200
  23. def OAI.RestrictedNerve.tripleDiagramResolutionHomologyIso line 205