CartanReducedCohomology.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Reduced unitary cohomology of the actual unimodular Cartan group

Root contraction proves sublinearity. Concrete controlled Følner pairs in the semidirect cover supply the averaging vectors, and compact lifts descend the uniform approximation to the original group.

theorem OAI.PolycyclicRecognition.cartan_unitary_reduced_vanishing line 39