OAI/Analysis/BoundedHochschild/TypeIIDefinitions.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Central projections and the finite type-II condition.

  1. def OAI.FinitePathMain.CentralProjection line 19
  2. def OAI.FinitePathMain.AbelianProjection line 22
  3. def OAI.FinitePathMain.TypeICentralSummand line 25
  4. def OAI.FinitePathMain.TypeII1 line 29
  5. def OAI.FinitePathMain.word line 33
  6. def OAI.FinitePathMain.signedValue line 36
  7. def OAI.FinitePathMain.pathValue line 39
  8. def OAI.FinitePathMain.FinitePathTests line 43
  9. def OAI.FinitePathMain.ProducerGoal line 55