OAI/NumberTheory/PiExponent/Approximation/InverseFrameRestriction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.InverseFrames.restrictPairing_pure line 12
2. lemma OAI.PiExponent.InverseFrames.inverseOpenFrame_pairing line 27
3. lemma OAI.PiExponent.InverseFrames.pairing_restrict line 35
4. lemma OAI.PiExponent.InverseFrames.restrictionMap_cycle line 48
5. lemma OAI.PiExponent.InverseFrames.inverseOpenFrame_restrict_pairing line 55
6. lemma OAI.PiExponent.InverseFrames.inverseOpenFrame_restrict line 81