OAI/GroupTheory/SimpleAmenable/Homology/E2Boundary.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.E2Leading.entry_inclusion line 18
  2. lemma OAI.E2Leading.entry_inclusion_ne line 22
  3. lemma OAI.E2Leading.lower_filtration line 27
  4. lemma OAI.E2Leading.lower_filtration' line 40
  5. lemma OAI.E2Leading.linear_units_smul line 46
  6. def OAI.E2Leading.lift line 50
  7. lemma OAI.E2Leading.lift_mem line 55
  8. lemma OAI.E2Leading.lift_left line 64
  9. lemma OAI.E2Leading.lift_right line 70
  10. lemma OAI.E2Leading.neg_pow_smul_twice line 76
  11. lemma OAI.E2Leading.d_lift_top line 81
  12. lemma OAI.E2Leading.d_lift_mem line 89
  13. lemma OAI.E2Leading.lead_zero_boundary line 124
  14. lemma OAI.E2Leading.finite_Eā‚‚ line 170
  15. lemma OAI.E2Leading.finite_total_concrete line 180
  16. lemma OAI.E2Leading.finite_total line 191