OAI/GroupTheory/PolycyclicRecognition/Finiteness/BicomplexSecondPageFiniteness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Total homology finiteness from the second page

Both kinds of leading boundary are removed explicitly: horizontal boundaries by row cycles, then vertical boundaries by the earlier column reduction.

  1. theorem OAI.PolycyclicRecognition.zero_secondPage_class_lowers_filtration line 18
  2. theorem OAI.PolycyclicRecognition.bicomplex_total_homology_finite_of_secondPage line 41