OAI/GroupTheory/PolycyclicRecognition/Analysis/CoarsePairMetricChange.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Uniform coarse-pair estimates under a change of compatible metric
- theorem
OAI.PolycyclicRecognition.coarse_pair_metric_changeline 10