OAI/NumberTheory/PiExponent/Approximation/ProjectionFormula.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ProjectionFormula.hom line 14
2. lemma OAI.PiExponent.ProjectionFormula.hom_pure line 21
3. lemma OAI.PiExponent.ProjectionFormula.naturality line 34
4. lemma OAI.PiExponent.ProjectionFormula.pullback_unit_apply line 49
5. lemma OAI.PiExponent.ProjectionFormula.unit_compatibility line 56
6. instance OAI.PiExponent.ProjectionFormula.unit_isIso line 77
7. lemma OAI.PiExponent.ProjectionFormula.framed_isIso line 88
8. lemma OAI.PiExponent.ProjectionFormula.restrict_compatibility line 100
9. instance OAI.PiExponent.ProjectionFormula.line_isIso line 138
10. def OAI.PiExponent.ProjectionFormula.iso line 154
11. def OAI.PiExponent.ProjectionFormula.twistIso line 159