OAI/NumberTheory/PiExponent/Cohomology/ProjectiveTwistCech.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.ProjectiveTwistCech.schemeFreeOpen line 16
2. structure OAI.PiExponent.ProjectiveTwistCech.LaurentCechPresentation line 18
3. def OAI.PiExponent.ProjectiveTwistCech.LaurentCechPresentation.toLaurent line 36
4. theorem OAI.PiExponent.ProjectiveTwistCech.LaurentCechPresentation.toLaurent_differential line 40
5. theorem OAI.PiExponent.ProjectiveTwistCech.LaurentCechPresentation.hasPrimitives line 54