OAI/GroupTheory/PolycyclicRecognition/Analysis/QuantitativeInjectiveCover.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Quantitative injective patches near nondegenerate derivatives
- theorem
OAI.PolycyclicRecognition.exists_quantitative_injective_coverline 15