OAI/NumberTheory/DukePrimeDegree/Geometry/RestrictedCoordinateMap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Restricting an embedded coordinate measure inside a second chart

  1. theorem OAI.DukePrimeDegree.map_restrict_comap_le line 12