OAI/NumberTheory/PiExponent/Approximation/NegativeTwistPresentations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.NegativeTwistPresentations.cancelIso line 15
2. def OAI.PiExponent.NegativeTwistPresentations.presentationMap line 24
3. instance OAI.PiExponent.NegativeTwistPresentations.presentationMap_epi line 28
4. def OAI.PiExponent.NegativeTwistPresentations.middleIsoBiproduct line 38
5. theorem OAI.PiExponent.NegativeTwistPresentations.middle_isFinitePresentation line 43
6. theorem OAI.PiExponent.NegativeTwistPresentations.kernel_isFinitePresentation line 50
7. theorem OAI.PiExponent.NegativeTwistPresentations.presentation_shortExact line 57
8. theorem OAI.PiExponent.NegativeTwistPresentations.middle_cohomology_finite line 62
9. def OAI.PiExponent.NegativeTwistPresentations.coherentFinitePresentation line 82