OAI/NumberTheory/PiExponent/Cohomology/ReesSheafCechNaturality.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.PiExponent.ReesSheafCechNaturality.chartMapline 30 - abbrev
OAI.PiExponent.ReesSheafCechNaturality.schemeFreeOpenline 38 - theorem
OAI.PiExponent.ReesSheafCechNaturality.chartOpen_leline 41 - theorem
OAI.PiExponent.ReesSheafCechNaturality.chartHomEquiv_restrictline 47 - theorem
OAI.PiExponent.ReesSheafCechNaturality.tupleHomEquiv_restrictline 71 - theorem
OAI.PiExponent.ReesSheafCechNaturality.cochainEquiv_differentialline 101