OAI/GroupTheory/PolycyclicRecognition/Algebra/VirtuallyMetabelianRecognition.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The cohomological recognition endgame for virtually metabelian groups

The virtually metabelian finiteness theorem supplies finite cohomological dimension, so duality transfer proves virtual polycyclicity.

  1. theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_coarse_PD_virtually_metabelian line 15