OAI/GroupTheory/SimpleAmenable/Simplicial/ConjugationNatural.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HomologyConjugation.rightBarLift line 15
  2. lemma OAI.HomologyConjugation.rightBarLift_single line 20
  3. lemma OAI.HomologyConjugation.bar_d_weighted line 25
  4. lemma OAI.HomologyConjugation.rightBarLift_d line 33
  5. def OAI.HomologyConjugation.rightBarMap line 55
  6. lemma OAI.HomologyConjugation.rightBarMap_π line 59
  7. def OAI.HomologyConjugation.rightBarHomotopy line 70
  8. def OAI.HomologyConjugation.conjugationCoeff line 78
  9. lemma OAI.HomologyConjugation.conjugationCoeff_apply line 85
  10. lemma OAI.HomologyConjugation.chainsIso_inv_weighted line 88
  11. lemma OAI.HomologyConjugation.conjugation_factorization line 96
  12. lemma OAI.HomologyConjugation.map_conjugation line 116
  13. lemma OAI.HomologyConjugation.map_after_conjugation line 135
  14. lemma OAI.HomologyConjugation.map_eq_of_centralizer line 142