OAI/GroupTheory/PolycyclicRecognition/Analysis/CoarseModelMean.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Amenability of the discrete group in the recognition argument

  1. theorem OAI.PolycyclicRecognition.invariantMean_of_coarse_virtualPolycyclic line 14