OAI/AlgebraicGeometry/SurfaceCones/
3985 declarations, 0 contain sorry, 0 declared as axioms; 66 files
Files
- AffineCanonicalCoordinates.lean 83 declarations
- AffineExteriorSections.lean 53 declarations
- AffineFrameSection.lean 63 declarations
- AffineLineEpiIso.lean 73 declarations
- AffineModelRank.lean 17 declarations
- AffineNaturalPower.lean 39 declarations
- Arithmetic.lean 6 declarations
- CMPuncture.lean 55 declarations
- CMReflexivity.lean 30 declarations
- CandidateRing.lean 1 declarations
- CanonicalConormal.lean 63 declarations
- CartierEquation.lean 60 declarations
- CartierFactorization.lean 60 declarations
- CartierGluing.lean 50 declarations
- CartierImageFiltration.lean 50 declarations
- CartierPullback.lean 58 declarations
- CartierSupport.lean 49 declarations
- ChartDominance.lean 92 declarations
- ClosedChartBaseChange.lean 57 declarations
- CoherentClosedFunctor.lean 53 declarations
- CoherentGlobalDual.lean 63 declarations
- CoherentGlobalHom.lean 52 declarations
- CoherentTensor.lean 41 declarations
- CompletedCartierNoetherian.lean 80 declarations
- CompletionParameters.lean 42 declarations
- ConeMorphism.lean 104 declarations
- CotangentCoordinates.lean 22 declarations
- CotangentSheaf.lean 51 declarations
- DeterminantTransport.lean 32 declarations
- ExteriorChangeScalars.lean 78 declarations
- ExteriorFunctor.lean 35 declarations
- ExteriorSheaf.lean 44 declarations
- GeometricChartSandwich.lean 48 declarations
- GlobalBaseChange.lean 5 declarations
- GradedCompletion.lean 25 declarations
- HomogeneousEvaluation.lean 70 declarations
- KummerCMRestriction.lean 60 declarations
- KummerCanonical.lean 27 declarations
- KummerCanonicalCharts.lean 58 declarations
- KummerCompletedBlowup.lean 81 declarations
- KummerGalois.lean 37 declarations
- KummerProjChart.lean 78 declarations
- KummerProjCover.lean 31 declarations
- KummerSectionAffineOpen.lean 117 declarations
- KummerShiftedDiagonalNormalization.lean 168 declarations
- KummerShiftedOpen.lean 174 declarations
- KummerSymmetry.lean 95 declarations
- KummerTripleDiagonalCoordinates.lean 180 declarations
- KummerTripleOpen.lean 160 declarations
- KummerUnramifiedNormalization.lean 106 declarations
- ModelSheaf.lean 3 declarations
- ModuleDepth.lean 29 declarations
- OriginTensor.lean 80 declarations
- PolynomialRangeTranscendence.lean 94 declarations
- PushforwardRestrictionNatural.lean 68 declarations
- ReesPunctureTopology.lean 32 declarations
- RestrictionRank.lean 6 declarations
- RingProperties.lean 23 declarations
- ScalarPullback.lean 53 declarations
- SectionCompletion.lean 107 declarations
- SectionFiniteChart.lean 97 declarations
- SpecCoordinates.lean 82 declarations
- SurfaceCharts.lean 8 declarations
- SurfaceSmooth.lean 8 declarations
- SwappedBaseChange.lean 64 declarations
- TensorLineCoherent.lean 55 declarations