OAI/GroupTheory/PolycyclicRecognition/Analysis/MetricFolnerUnimodular.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Metric Følner sets force right invariance of Haar measure

Right translation moves every point a fixed distance in a left invariant metric. A nontrivial modular character contradicts the neighborhood-volume ratio tending to one.

  1. theorem OAI.PolycyclicRecognition.isMulRightInvariant_of_metricFolner line 21