OAI/NumberTheory/PiExponent/Approximation/LinePullbackPowers.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponentSeshadri.PullbackTensor.hom line 13
2. lemma OAI.PiExponentSeshadri.PullbackTensor.unit_hom line 20
3. lemma OAI.PiExponentSeshadri.PullbackTensor.naturality line 28
4. lemma OAI.PiExponentSeshadri.PullbackTensor.unit_pure_structure line 40
5. lemma OAI.PiExponentSeshadri.PullbackTensor.unit_compatibility line 46
6. instance OAI.PiExponentSeshadri.PullbackTensor.unit_isIso line 98
7. lemma OAI.PiExponentSeshadri.PullbackTensor.open_transpose line 112
8. lemma OAI.PiExponentSeshadri.PullbackTensor.restrict_compatibility line 120
9. lemma OAI.PiExponentSeshadri.PullbackTensor.framed_isIso line 166
10. instance OAI.PiExponentSeshadri.PullbackTensor.power_step_isIso line 182
11. def OAI.PiExponentSeshadri.PullbackTensor.powIso line 209