OAI/NumberTheory/PiExponent/Approximation/InverseFrames.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.InverseFrames.regularValue line 12
2. def OAI.PiExponent.InverseFrames.pairingFrame line 15
3. lemma OAI.PiExponent.InverseFrames.unit_inv_pure line 18
4. lemma OAI.PiExponent.InverseFrames.pairingFrame_apply line 32
5. lemma OAI.PiExponent.InverseFrames.frame_generator_change line 42
6. lemma OAI.PiExponent.InverseFrames.pairingFrame_change_apply line 52
7. lemma OAI.PiExponent.InverseFrames.pairingFrame_frameChange line 68
8. lemma OAI.PiExponent.InverseFrames.pairing_apply line 81
9. lemma OAI.PiExponent.InverseFrames.pairing_inverse_generator line 103
10. def OAI.PiExponent.InverseFrames.dualMap line 114
11. lemma OAI.PiExponent.InverseFrames.dualMap_apply line 117
12. lemma OAI.PiExponent.InverseFrames.dualMap_coefficient line 126
13. def OAI.PiExponent.InverseFrames.restrictPairing line 133
14. def OAI.PiExponent.InverseFrames.inverseOpenFrame line 138
15. lemma OAI.PiExponent.InverseFrames.inverseOpenFrame_frameChange line 142