OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanGoodRootNeighborLabels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Root-neighbor label equality from the diagonal's retained good sets

The relative Haar mass may decay subexponentially. No positive limiting fraction or supported point of the full sampling law is required.

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.good_root_neighbor_labels_eq line 38