OAI/GroupTheory/PolycyclicRecognition/Analysis/CoarseModelUnimodular.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Unimodularity of the Lie model follows from the original comparison group

The quasi-isometry contributes its lower bound and coarse surjectivity. Polycyclicity contributes a proved invariant mean; no model-unimodularity hypothesis is retained.

  1. theorem OAI.PolycyclicRecognition.isMulRightInvariant_of_coarse_virtualPolycyclic line 19