OAI/NumberTheory/DukePrimeDegree/Geometry/RadialLocalInjectivity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The radial future lift is inside an injective quotient chart

  1. theorem OAI.DukePrimeDegree.exists_radial_radius_injective_triangular_lifts line 13