OAI/NumberTheory/PiExponent/Approximation/TwistPresentations.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.GeometrySupport.TwistPresentations.schemeUnit line 12
2. def OAI.PiExponent.GeometrySupport.TwistPresentations.twistShiftIso line 17
3. def OAI.PiExponent.GeometrySupport.TwistPresentations.twistFreeIsoBiproduct line 22
4. abbrev OAI.PiExponent.GeometrySupport.TwistPresentations.presentationKernel line 34
5. abbrev OAI.PiExponent.GeometrySupport.TwistPresentations.presentationMiddle line 36
6. def OAI.PiExponent.GeometrySupport.TwistPresentations.presentationLeft line 39
7. def OAI.PiExponent.GeometrySupport.TwistPresentations.presentationRight line 43
8. theorem OAI.PiExponent.GeometrySupport.TwistPresentations.presentation_comp_zero line 47
9. theorem OAI.PiExponent.GeometrySupport.TwistPresentations.presentation_shortExact line 52
10. theorem OAI.PiExponent.GeometrySupport.TwistPresentations.presentationKernel_isFinitePresentation line 74
11. theorem OAI.PiExponent.GeometrySupport.TwistPresentations.presentationMiddle_ext_zero line 82
12. def OAI.PiExponent.GeometrySupport.TwistPresentations.coherentTwistFamily line 100
13. def OAI.PiExponent.GeometrySupport.TwistPresentations.acyclicPresentationOfGenerators line 104