OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianQuotientFiniteDimension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite virtual dimension above an abelian quotient

Only the kernel's actual integral cohomological dimension is used. The kernel may be infinitely generated.

  1. theorem OAI.PolycyclicRecognition.abelian_quotient_virtual_finite_dimension line 17