`OAI/NumberTheory/PiExponent/Geometry/`

1363 declarations, 0 contain sorry, 0 declared as axioms; 181 files

Files

AdmissibleCurveCoordinates.lean 16 declarations
AdmissibleCurveDegreeData.lean 2 declarations
AdmissibleCurveImage.lean 7 declarations
AdmissibleCurveInequality.lean 3 declarations
AdmissibleCurveModel.lean 2 declarations
AdmissibleCurveWeights.lean 16 declarations
BirationalOpenIso.lean 1 declarations
BirationalValuationStalk.lean 4 declarations
CanonicalRecoveryProperties.lean 4 declarations
CartierDegreeLength.lean 1 declarations
CartierPowerFrames.lean 8 declarations
CartierSequence.lean 3 declarations
CoherentProjectiveFinite.lean 4 declarations
ConePrimeProperties.lean 7 declarations
CurveCenters.lean 12 declarations
CurveChartFunctionField.lean 4 declarations
CurveComponentCutLengths.lean 2 declarations
CurveComponentIncidence.lean 2 declarations
CurveComponentLocalLengths.lean 5 declarations
CurveComponentMultiplicity.lean 8 declarations
CurveComponentRigidity.lean 5 declarations
CurveComponentStalks.lean 8 declarations
CurveComponentZeroPoints.lean 4 declarations
CurveComponentsDimension.lean 4 declarations
CurveContact.lean 14 declarations
CurveContactFamily.lean 17 declarations
CurveContactSum.lean 19 declarations
CurveCutQuotient.lean 3 declarations
CurveCycleLengths.lean 3 declarations
CurveCycleNumerical.lean 6 declarations
CurveDegreeAdditivity.lean 11 declarations
CurveDegreeLaws.lean 6 declarations
CurveEffectiveTwist.lean 7 declarations
CurveFieldRigidity.lean 6 declarations
CurveFinitePushforwardCoherent.lean 4 declarations
CurveFunctionFieldCompatibility.lean 7 declarations
CurveGeometricFunctionField.lean 11 declarations
CurveGlobalCoordinateOrder.lean 2 declarations
CurveGlobalMonomial.lean 3 declarations
CurveGlobalMonomialLocal.lean 9 declarations
CurveImageAffineChart.lean 6 declarations
CurveImageAffineCoordinates.lean 7 declarations
CurveImageOpenLocus.lean 2 declarations
CurveInequality.lean 3 declarations
CurveInequalityIntrinsic.lean 3 declarations
CurveLocalAssociativity.lean 4 declarations
CurveLocalMultiplicity.lean 3 declarations
CurveLocalOrder.lean 24 declarations
CurveModelFieldEmbedding.lean 7 declarations
CurveModelGenericPoint.lean 10 declarations
CurveModelInfinityGenericPoint.lean 1 declarations
CurveModelLocalOrder.lean 7 declarations
CurveModelPlaces.lean 30 declarations
CurveMonomialMap.lean 4 declarations
CurveMorphismFinite.lean 4 declarations
CurveNormalizationDegree.lean 7 declarations
CurveNormalizationDimension.lean 7 declarations
CurveNormalizationInvariance.lean 3 declarations
CurveNormalizationLocalRing.lean 7 declarations
CurveNormalizationModel.lean 34 declarations
CurveNormalizationMorphism.lean 9 declarations
CurveNormalizationNonaffine.lean 1 declarations
CurveNormalizationOverlap.lean 4 declarations
CurveNormalizationProjective.lean 3 declarations
CurveNormalizationProper.lean 13 declarations
CurveNormalizationUnit.lean 6 declarations
CurveNormalizedDegreeTransfer.lean 3 declarations
CurveParameterFinite.lean 2 declarations
CurvePlaceCenter.lean 8 declarations
CurvePlaceCenterStalk.lean 5 declarations
CurvePlaceSectionDivisor.lean 4 declarations
CurvePlaceSectionOrder.lean 1 declarations
CurvePrimeHeight.lean 7 declarations
CurveProductFormula.lean 14 declarations
CurveProperExtension.lean 3 declarations
CurveProperImageDimension.lean 6 declarations
CurveSectionDegree.lean 6 declarations
CurveStalkGluing.lean 6 declarations
CurveValuationCenter.lean 29 declarations
CurveZeroPole.lean 47 declarations
FiniteCurveZeros.lean 15 declarations
FiniteNormalizationGrowth.lean 12 declarations
FiniteOfNoContractedCurves.lean 4 declarations
FromSpecStalkLocalIso.lean 3 declarations
GeneralCartierDegreeLength.lean 3 declarations
IdealSheafPowers.lean 2 declarations
IntegralCurveExistence.lean 7 declarations
LineBundleCoherent.lean 4 declarations
LineBundleFrameCocycle.lean 13 declarations
LineBundleGluing.lean 26 declarations
LineBundleGluingSections.lean 7 declarations
LineBundleGluingTransitions.lean 5 declarations
LineBundleInverse.lean 9 declarations
LineBundleProduct.lean 4 declarations
LineBundleTensor.lean 37 declarations
NormalizationGrowth.lean 5 declarations
PlaceCenteredBranch.lean 16 declarations
PlaceLocalRing.lean 5 declarations
PlaceParameterModel.lean 9 declarations
PlaceValuationRing.lean 8 declarations
PolynomialProjectiveStructure.lean 5 declarations
PrincipalCartierSequence.lean 3 declarations
ProjectiveChartOverlaps.lean 7 declarations
ProjectiveChartRingNaturality.lean 7 declarations
ProjectiveChartRingNaturalityCore.lean 10 declarations
ProjectiveChartSections.lean 15 declarations
ProjectiveCharts.lean 25 declarations
ProjectiveCoefficientBound.lean 3 declarations
ProjectiveCoordinateChartMap.lean 3 declarations
ProjectiveCoordinateConstants.lean 4 declarations
ProjectiveCoordinateFinite.lean 3 declarations
ProjectiveCoordinateFiniteSections.lean 9 declarations
ProjectiveCoordinateFiniteValues.lean 8 declarations
ProjectiveCoordinateOverlapNaturality.lean 1 declarations
ProjectiveCoordinatePullback.lean 6 declarations
ProjectiveCoordinateRatios.lean 11 declarations
ProjectiveCoordinateRingNaturality.lean 8 declarations
ProjectiveCoordinateScalars.lean 7 declarations
ProjectiveCoordinateSections.lean 13 declarations
ProjectiveCoordinateTransitions.lean 5 declarations
ProjectiveCoordinateValues.lean 4 declarations
ProjectiveCoordinates.lean 32 declarations
ProjectiveCurveTwoAffine.lean 7 declarations
ProjectiveDenseChart.lean 4 declarations
ProjectiveEmbeddingCharts.lean 13 declarations
ProjectiveFiniteCoordinates.lean 4 declarations
ProjectiveFinitePencil.lean 11 declarations
ProjectiveFrameNaturality.lean 4 declarations
ProjectiveFramedAtlas.lean 4 declarations
ProjectiveFramedSections.lean 10 declarations
ProjectiveGlobalPolynomialAlgebra.lean 6 declarations
ProjectiveGlobalPolynomials.lean 17 declarations
ProjectiveIntrinsicCoefficientLaw.lean 15 declarations
ProjectiveLatticeOrder.lean 2 declarations
ProjectiveLatticePullback.lean 5 declarations
ProjectiveLineCharts.lean 16 declarations
ProjectiveLineProper.lean 7 declarations
ProjectiveLineReciprocal.lean 6 declarations
ProjectiveLocalCoefficients.lean 3 declarations
ProjectiveMonomialFinite.lean 12 declarations
ProjectiveNegativeCoordinates.lean 3 declarations
ProjectiveNegativeFrames.lean 3 declarations
ProjectiveNegativeScalars.lean 4 declarations
ProjectiveNegativeTransitions.lean 3 declarations
ProjectiveO1ChartMap.lean 11 declarations
ProjectiveO1Identity.lean 2 declarations
ProjectiveO1LocalIdentity.lean 1 declarations
ProjectiveO1Morphism.lean 4 declarations
ProjectiveO1Sections.lean 7 declarations
ProjectivePencilScalars.lean 3 declarations
ProjectivePullbackFrames.lean 5 declarations
ProjectiveRatioCocycle.lean 9 declarations
ProjectiveRepresentedCoefficient.lean 2 declarations
ProjectiveSectionExtension.lean 4 declarations
ProjectiveSectionInterface.lean 8 declarations
ProjectiveSectionPullback.lean 6 declarations
ProjectiveSectionReindex.lean 8 declarations
ProjectiveSectionsPullback.lean 4 declarations
ProjectiveSerreTransfer.lean 3 declarations
ProjectiveSpaceBasics.lean 4 declarations
ProjectiveSpaceFinite.lean 3 declarations
ProjectiveSpaceIntegral.lean 3 declarations
ProjectiveSpaceSerre.lean 3 declarations
ProjectiveTupleCharts.lean 14 declarations
ProjectiveVertexCompatibility.lean 2 declarations
ProperHypersurfaceHilbert.lean 3 declarations
ReducedComponentStalk.lean 9 declarations
SectionCartierPower.lean 5 declarations
SectionCartierRegular.lean 5 declarations
SectionOrderDivisor.lean 9 declarations
SectionZeroStalk.lean 7 declarations
SheafSectionGluing.lean 7 declarations
SheafificationUnitIso.lean 2 declarations
SupportedSheaf.lean 4 declarations
WeightedCurveDegree.lean 25 declarations
WeightedCurveRigidity.lean 3 declarations
WeightedLocalSheaf.lean 11 declarations
WeightedProjectiveCurveDegree.lean 2 declarations
WeightedProjectiveEmbedding.lean 6 declarations
WeightedProjectiveLineBundle.lean 4 declarations
WeightedProjectiveStructure.lean 3 declarations