OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalExtensionDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The rational dimension bound for an actual group extension

The finite total-complex comparison gives the sum of the kernel and quotient bounds for every coefficient representation.

  1. def OAI.PolycyclicRecognition.coefficientNormalSecondPageIso line 17
  2. theorem OAI.PolycyclicRecognition.rational_homology_bound_of_extension line 28