Machine-generated inventory

Source exposition

A commit-pinned map from canonical roadmap artifacts to checked Lean modules. Complete declaration, import, roadmap-state, and cache-partition metadata is available in JSON.

87Roadmap-linked modules
456Supporting source
1,342Unlinked cache-heavy certificate modules

Search every source name

Search all 1,885 modules, declaration names, import names, and mapped roadmap artifacts. This includes the cache-heavy modules collapsed in the tables below.

Loading the compact search index…

    Roadmap-linked modules

    These modules are named by canonical artifacts in coordination/program.json. States shown here are artifact states, not inferred from source text. 211 of 292 artifacts currently record an indexed local module; proposed artifacts without a module remain visible in the complete JSON roadmap index.

    ModuleLinesDeclarationsImportsRoadmap artifacts
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleCohomology449324AlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleFiniteFlatGroup contract · MT-FFGS-CONNECTED-ETALE
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleFiltration275132AlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleFiltrationStep.baseChange_point_pow_sq_eq_one integrated · MT-FFGS-BASICAlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleSimpleFactor.baseChange integrated · MT-FFGS-BASIC
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.Affine2,0811649AlgebraicGeometry.AffineFiniteFlatCommGroupScheme.point_pow_eq_one_of_constantRank integrated · MT-FFGS-BASIC
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.Basic832805AlgebraicGeometry.FiniteFlatCommGroupScheme integrated · MT-FFGS-BASICAlgebraicGeometry.FiniteFlatCommGroupScheme.KernelPresentation.baseChange integrated · MT-FFGS-BASICAlgebraicGeometry.FiniteFlatCommGroupScheme.kernel integrated · MT-FFGS-BASICAlgebraicGeometry.FiniteFlatCommGroupScheme.kernelPresentation_exists_of_finite_flat integrated · MT-FFGS-BASIC
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemeFppfHOne9081AlgebraicGeometry.CommGroupScheme.FppfHOne contract · MT-FFGS-CONNECTED-ETALEAlgebraicGeometry.CommGroupScheme.pointPresheaf_isFppfSheaf contract · MT-FFGS-CONNECTED-ETALE
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemePowerKummerTorsionRankZero16882AlgebraicGeometry.FiniteFlatCommGroupScheme.finrank_additive_basePoint_eq_zero_of_powerKummer_kernelData contract · MT-FFGS-OORT-RAYNAUD
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FiniteTranslationQuotientGeometry405128AlgebraicGeometry.FiniteTranslationQuotient.structureMap_geometricallyIntegral contract · MT-EC-ISOGENY-WEILAlgebraicGeometry.FiniteTranslationQuotient.structureMap_isProper contract · MT-EC-ISOGENY-WEILAlgebraicGeometry.FiniteTranslationQuotient.structureMap_smooth_of_flat contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfHOne586655AlgebraicGeometry.Scheme.FppfHOne contract · MT-FFGS-CONNECTED-ETALE
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfHOneFunctoriality518541AlgebraicGeometry.CommGroupScheme.fppfHOneMap contract · MT-FFGS-CONNECTED-ETALE
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfKummerRankZero16943AlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleFiltrationStep.finite_of_fppfKummer_int contract · MT-FFGS-OORT-RAYNAUDAlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleFiltrationStep.finrank_eq_zero_of_fppfKummer_int contract · MT-FFGS-OORT-RAYNAUDAlgebraicGeometry.FiniteFlatCommGroupScheme.finite_of_injective_kummer_of_card_le_torsion contract · MT-FFGS-OORT-RAYNAUDAlgebraicGeometry.FiniteFlatCommGroupScheme.finrank_eq_zero_of_injective_kummer_of_card_le_torsion contract · MT-FFGS-OORT-RAYNAUD
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.Quotient233192AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfQuotientPresentation contract · MT-FFGS-BASICAlgebraicGeometry.FiniteFlatCommGroupScheme.FppfQuotientPresentation.baseChangePresentation integrated · MT-FFGS-BASIC
    MazurTorsion.AlgebraicGeometry.FormalCompletion214143AlgebraicGeometry.IsFormalImmersionAt contract · MT-X0-INTEGRAL
    MazurTorsion.AlgebraicGeometry.FormalImmersionSpecialFiber506161AlgebraicGeometry.Scheme.Hom.isFormalImmersionAt_of_mappedIdealCotangentSurjective contract · MT-X0-INTEGRALAlgebraicGeometry.Scheme.Hom.isFormalImmersionAt_of_quotientCotangentCertificate contract · MT-X0-INTEGRALIsLocalRing.QuotientCotangentCertificate contract · MT-X0-INTEGRALIsLocalRing.cotangentMap_surjective_of_quotientCotangentCertificate contract · MT-X0-INTEGRAL
    MazurTorsion.AlgebraicGeometry.NeronModel.Basic198174AlgebraicGeometry.NeronModel contract · MT-NERON-BASEAlgebraicGeometry.NeronModel.sectionExtension contract · MT-NERON-BASE
    MazurTorsion.AlgebraicGeometry.NeronModel.PowerKernelKummerRankZero7732AlgebraicGeometry.NeronModel.finrank_genericBasePoint_eq_zero_of_powerKummer_kernelData contract · MT-NERON-SPECIALIZATION
    MazurTorsion.AlgebraicGeometry.NeronModel.ProperModelBasePoint234182AlgebraicGeometry.ProperModelBasePoint.mulEquiv contract · MT-NERON-BASE
    MazurTorsion.AlgebraicGeometry.NeronModel.Specialization206151AlgebraicGeometry.ProperModelBasePoint.basePointSpecialization contract · MT-NERON-SPECIALIZATIONAlgebraicGeometry.ProperModelBasePoint.basePoint_eq_of_restrict_eq_of_generic_torsion contract · MT-NERON-SPECIALIZATION
    MazurTorsion.AlgebraicGeometry.PicardAbelJacobi803383MazurTorsion.AlgebraicGeometry.PicardGroup.setOf_weightedAbelJacobiDivisorClass_one_effectiveDivisorOfDegree_eq contract · MT-TC-C2-SYMMETRIC-POWERSMazurTorsion.AlgebraicGeometry.PicardGroup.setOf_weightedAbelJacobiDivisorClass_one_ofSym_eq contract · MT-TC-C2-SYMMETRIC-POWERSMazurTorsion.AlgebraicGeometry.PicardGroup.weightedAbelJacobiDivisorClass_one_effectiveDivisorOfDegree_eq_iff_mem_completeLinearSystem contract · MT-TC-C2-SYMMETRIC-POWERSMazurTorsion.AlgebraicGeometry.PicardGroup.weightedAbelJacobiDivisorClass_one_ofSym_eq_iff_mem_completeLinearSystem contract · MT-TC-C2-SYMMETRIC-POWERSMazurTorsion.AlgebraicGeometry.PicardGroup.coe_weightedBasepointChangeClass contract · MT-TC-F1-ABEL-JACOBIMazurTorsion.AlgebraicGeometry.PicardGroup.weightedAbelJacobiClass_change_base contract · MT-TC-F1-ABEL-JACOBIMazurTorsion.AlgebraicGeometry.PicardGroup.weightedAbelJacobiClass_oldBase_eq_weightedBasepointChangeClass contract · MT-TC-F1-ABEL-JACOBIMazurTorsion.AlgebraicGeometry.PicardGroup.weightedAbelJacobiDivisorClass_change_base contract · MT-TC-F1-ABEL-JACOBIMazurTorsion.AlgebraicGeometry.PicardGroup.weightedBasepointChangeClass contract · MT-TC-F1-ABEL-JACOBI
    MazurTorsion.AlgebraicGeometry.PicardDegreeZero493313MazurTorsion.AlgebraicGeometry.CurveDivisorDescent.DivisorCocycleSystem.ExplicitInverse.degreeZero contract · MT-TC-D1-PICARD-FUNCTORMazurTorsion.AlgebraicGeometry.CurveDivisorDescent.DivisorCocycleSystem.ExplicitInverse.divisorToPic_mem_degreeZero_iff contract · MT-TC-D1-PICARD-FUNCTORMazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.degreeZero contract · MT-TC-D1-PICARD-FUNCTORMazurTorsion.AlgebraicGeometry.DivisorPicard.Dictionary.degreeZeroRepresentative contract · MT-TC-D1-PICARD-FUNCTORMazurTorsion.AlgebraicGeometry.PicardGroup.properCurveDegreeHom contract · MT-TC-D1-PICARD-FUNCTORMazurTorsion.AlgebraicGeometry.PicardGroup.properCurveDegreeZero_eq_ker contract · MT-TC-D1-PICARD-FUNCTORMazurTorsion.AlgebraicGeometry.PicardGroup.properCurvePicardAddEquivDegreeZeroProdInt contract · MT-TC-D1-PICARD-FUNCTOR
    MazurTorsion.AlgebraicGeometry.PicardRationalSectionAbelJacobi350235MazurTorsion.AlgebraicGeometry.PicardGroup.rationalSectionAbelJacobiDegreeKernel contract · MT-TC-D1-PICARD-FUNCTORMazurTorsion.AlgebraicGeometry.PicardGroup.rationalSectionAbelJacobiPicRelFppfClass contract · MT-TC-D1-PICARD-FUNCTORMazurTorsion.AlgebraicGeometry.PicardGroup.rationalSectionPicardAddEquivDegreeZeroProdInt contract · MT-TC-D1-PICARD-FUNCTOR
    MazurTorsion.AlgebraicGeometry.RelativePicardFppf12675AlgebraicGeometry.Scheme.Modules.picRelFppfSheaf contract · MT-TC-D1-PICARD-FUNCTORAlgebraicGeometry.Scheme.Modules.properCurveDegreeKernelToPicRelFppfAtBase contract · MT-TC-D1-PICARD-FUNCTOR
    MazurTorsion.Arithmetic.CardinalityReduction6634MazurTorsion.torsion_ncard_le_of_explicit_arithmetic integrated · MT-BASE-INTEGRATED
    MazurTorsion.Arithmetic.PointOrder237117MazurTorsion.rationalTorsion_orders_mem_cyclicOrders_of_remaining_obstructions integrated · MT-BASE-INTEGRATEDMazurTorsion.remainingKubertForbiddenOrders integrated · MT-BASE-INTEGRATED
    MazurTorsion.Arithmetic.RankTwoReduction10064MazurTorsion.rationalTorsion_finite integrated · MT-BASE-INTEGRATEDMazurTorsion.rationalTorsion_hasRankTwoPresentation contract · MT-FINAL-ASSEMBLY
    MazurTorsion.EllipticCurve.NonsingularReduction328191WeierstrassCurve.Affine.HasNonsingularReduction contract · MT-NERON-COMPONENTSWeierstrassCurve.Affine.nonsingularReduction contract · MT-NERON-COMPONENTS
    MazurTorsion.EllipticCurve.TameAdditiveReductionData327213MazurTorsion.EllipticCurve.TameAdditiveReductionData contract · MT-NERON-COMPONENTSMazurTorsion.EllipticCurve.TameAdditiveReductionDataAtEleven contract · MT-NERON-COMPONENTSMazurTorsion.EllipticCurve.TameAdditiveReductionDataAtFive contract · MT-NERON-COMPONENTSMazurTorsion.EllipticCurve.TameAdditiveReductionDataAtFive.toTameAdditiveFiltrationData contract · MT-PRIME-HERBRAND-KUMMER
    MazurTorsion.Foundations.NaiveHeightDescent414228WeierstrassCurve.Affine.approx_parallelogram_law integrated · MT-BASE-INTEGRATED
    MazurTorsion.GroupTheory.ClassificationCardinality7873MazurTorsion.RationalTorsion integrated · MT-BASE-INTEGRATEDMazurTorsion.cyclicOrders integrated · MT-BASE-INTEGRATED
    MazurTorsion.GroupTheory.FiniteClassification515233MazurTorsion.exists_rankTwoPresentation_of_allowed_orders_and_forbidden integrated · MT-BASE-INTEGRATED
    MazurTorsion.Kubert.OrderElevenModelInverse512312MazurTorsion.Kubert.exists_elliptic_tate_marked_order_eleven_of_model contract · MT-X11-COSETMazurTorsion.Kubert.model_abscissa_eq_zero_or_one_of_no_order_eleven contract · MT-X11-COSETMazurTorsion.Kubert.orderElevenModelOfRaw_inverse contract · MT-X11-COSET
    MazurTorsion.Kubert.OrderThirtyFiveFiniteField6333MazurTorsion.OrderThirtyFive.card_reductionAtEleven_le_eighteen contract · MT-O35-EXCLUDE
    MazurTorsion.Kubert.OrderThirtyFiveFiniteFieldOrder7951MazurTorsion.OrderThirtyFive.shortCurveEleven_addOrderOf_le_eighteen contract · MT-O35-EXCLUDEMazurTorsion.OrderThirtyFive.shortCurveEleven_addOrderOf_ne_of_nineteen_le contract · MT-O35-EXCLUDEMazurTorsion.OrderThirtyFive.zmod_eleven_addOrderOf_le_eighteen contract · MT-O35-EXCLUDEMazurTorsion.OrderThirtyFive.zmod_eleven_addOrderOf_ne_of_nineteen_le contract · MT-O35-EXCLUDE
    MazurTorsion.Kubert.OrderTwentyFive22971MazurTorsion.Kubert.exists_tateOrderTwentyFive_recurrence_certificate contract · MT-O25-EXCLUDEMazurTorsion.Kubert.orderTwentyFiveClearedEquation_eq_zero_of_marked_order contract · MT-O25-EXCLUDEMazurTorsion.Kubert.orderTwentyFiveRecurrenceEquation_eq_zero_of_marked_order contract · MT-O25-EXCLUDEMazurTorsion.Kubert.tateSuccessiveX_ne_zero_of_marked_order_twentyFive contract · MT-O25-EXCLUDE
    MazurTorsion.Kubert.OrderTwentyFiveNormalizedModel2,5681602MazurTorsion.Kubert.exists_tateOrderTwentyFive_noncuspidal_certificate contract · MT-O25-EXCLUDEMazurTorsion.Kubert.orderTwentyFiveNoncuspidalFactor_eq_zero_of_marked_order contract · MT-O25-EXCLUDEMazurTorsion.Kubert.orderTwentyFive_normalized_collision_factorization contract · MT-O25-EXCLUDE
    MazurTorsion.Kubert.TateNormalFormMultiples310221MazurTorsion.Kubert.nsmul_origin_eq_successiveCoordinates contract · MT-O25-EXCLUDEMazurTorsion.Kubert.tateClearedCoordinates_spec contract · MT-O25-EXCLUDE
    MazurTorsion.ModularCurve.AffineCuspPolynomialChart500301MazurTorsion.ModularCurve.AffineCuspPolynomialChart.sectionAt contract · MT-X0-INTEGRALMazurTorsion.ModularCurve.AffineCuspPolynomialChart.sectionAt_closedPoint_eq_zeroSection contract · MT-X0-INTEGRALMazurTorsion.ModularCurve.AffineCuspPolynomialChart.valuation_j_le_one_of_polynomialCuspSectionAtFive contract · MT-X0-INTEGRAL
    MazurTorsion.ModularCurve.CompleteDVRCoordinate255124MazurTorsion.ModularCurve.DegreeOneCotangentCertificate.specMap_fromStalk_eq_of_completeDVR_normalizedQExpansion contract · MT-X0-HECKE
    MazurTorsion.ModularCurve.HeckeFirstCoefficient24053MazurTorsion.ModularCurve.DegreeOneCotangentCertificate.isFormalImmersionAt_of_heckeEigen_qExpansion contract · MT-X0-HECKEMazurTorsion.ModularCurve.DegreeOneCotangentCertificate.isFormalImmersionAt_of_rationalSection_heckeEigen_qExpansion contract · MT-X0-HECKEMazurTorsion.ModularCurve.HeckeFirstCoefficient.coeff_one_ne_zero_of_simultaneousEigenvector contract · MT-X0-HECKE
    MazurTorsion.ModularCurve.NeronSectionSpecialization21833MazurTorsion.PrimeOrder.rationalPoint_primeOrder_ne_of_properModelSpecializationAtFive contract · MT-PRIME-EISENSTEIN-SPECIALIZATION
    MazurTorsion.ModularCurve.QExpansionFirstCoefficient23673MazurTorsion.ModularCurve.DegreeOneCotangentCertificate.isFormalImmersionAt_of_smoothRelativeCurve_rationalPoint_of_normalizedQExpansion contract · MT-X0-HECKEMazurTorsion.ModularCurve.DegreeOneCotangentCertificate.specMap_fromStalk_eq_of_normalizedQExpansion contract · MT-X0-HECKE
    MazurTorsion.ModularCurve.XZeroCyclicQuotient253231MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.PointQuotient contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.dualMap contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.dualMap_comp_quotientMap contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.quotientMap contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.quotientMap_comp_dualMap contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroEllipticQuotientGeometry11762AlgebraicGeometry.FiniteTranslationQuotient.abelianVarietyOfAbelianVariety contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroModuli559442MazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup contract · MT-X0-MODULIMazurTorsion.ModularCurve.XZeroModuli.RationalCyclicSubgroup.divisorSubgroup contract · MT-X0-MODULIMazurTorsion.ModularCurve.XZeroModuli.RationalDatum.VariableChangeClass contract · MT-X0-MODULIMazurTorsion.ModularCurve.XZeroModuli.RationalDatum.VariableChangeClass.lift contract · MT-X0-MODULIMazurTorsion.ModularCurve.XZeroModuli.RationalDatum.variableChange contract · MT-X0-MODULI
    MazurTorsion.ModularCurve.XZeroWeierstrassAdditionAtlas647371MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.affinePairAdditionCharts_cover contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.affinePairAdditionMorphism contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassAntidiagonalAdditionMorphism1,170511MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.antidiagonalAdditionProjectiveMorphism contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.productAntidiagonalIntersection_additionProjective_eq contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassCrossCompatibility875441MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.productVerticalIntersection_additionProjective_eq contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.secantAntidiagonalIntersection_additionProjective_eq contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassInfinityCompatibility297111MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.infinityIntersection_additionProjective_eq contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassProductNeighborhoodAddition1,216973MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.productNeighborhoodAdditionOnProductOpen contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.productNeighborhoodAdditionProjectiveMorphism_comp_structureMap contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.productNeighborhoodProductOpen contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassProductNeighborhoodCompatibility4611MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.productNeighborhoodAddition_secant_and_tangent_compatible contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassProjectiveProductAtlas169142MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.projectivePairOpenCover contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.standardPairAdditionMorphism contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.standardPairIsoAffinePair contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassSecantAdditionMorphism412374MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.secantAdditionOnProductOpen contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.secantAdditionOnProductOpen_comp_structureMap contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.secantProductOpen contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassTangentAdditionMorphism192153MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.tangentChartToAffineCurve_opensRange contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.tangentDoublingProjectiveMorphism contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.tangentDoublingProjectiveMorphism_comp_structureMap contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.ModularCurve.XZeroWeierstrassVerticalAdditionMorphism536352MazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.secantVerticalIntersection_additionProjective_eq contract · MT-EC-ISOGENY-WEILMazurTorsion.ModularCurve.XZeroFiniteFlatModuli.WeierstrassProjectiveCubic.verticalAdditionProjectiveMorphism contract · MT-EC-ISOGENY-WEIL
    MazurTorsion.NumberTheory.CyclotomicCapitulation243132NumberTheory.CyclotomicCharacter.InverseExtension.capitulationHom contract · MT-CYCLOTOMIC-UNRAMIFIEDNumberTheory.CyclotomicCharacter.InverseExtension.capitulationHom_equivariant contract · MT-CYCLOTOMIC-UNRAMIFIEDNumberTheory.CyclotomicCharacter.InverseExtension.exists_nontrivial_p_torsion_capitulating_orbit contract · MT-CYCLOTOMIC-UNRAMIFIED
    MazurTorsion.NumberTheory.RatNorthcott6122MazurTorsion.rationalLogHeightNorthcott integrated · MT-BASE-INTEGRATED
    MazurTorsion.NumberTheory.XOneEighteenEisensteinIntegers719292MazurTorsion.XOneEighteenDescent.TwoPrimeSupportedEisensteinIntegerFiniteSplitCyclicCubicObstruction contract · MT-X18-NONCUSPMazurTorsion.XOneEighteenDescent.rationalPoint_addOrderOf_ne_eighteen_of_twoPrimeSupportedEisensteinIntegerObstruction contract · MT-X18-NONCUSPMazurTorsion.XOneEighteenDescent.splitEisensteinThreePrime_not_common contract · MT-X18-NONCUSP
    MazurTorsion.NumberTheory.XOneEighteenQuadraticNorm16842MazurTorsion.XOneEighteenDescent.antiDiagonalZ_sq_of_fourScalarCorrespondence contract · MT-X18-NONCUSP
    MazurTorsion.NumberTheory.XOneEighteenQuadraticNormBase664422MazurTorsion.XOneEighteenDescent.antiDiagonalExceptionalPolynomial_ne_zero contract · MT-X18-NONCUSP
    MazurTorsion.NumberTheory.XOneElevenFiveIsogenyHom9361MazurTorsion.XOneEleven.veluFiveMap_eq_zero_iff_five_nsmul contract · MT-X11-COSET
    MazurTorsion.NumberTheory.XOneElevenFiveSelmer10053MazurTorsion.XOneEleven.exists_fifthPower_of_emptyFiveSelmer contract · MT-X11-COSET
    MazurTorsion.NumberTheory.XOneElevenUniformCoset10632MazurTorsion.XOneEleven.fiveCosetBound_of_no_order_eleven contract · MT-X11-COSET
    MazurTorsion.NumberTheory.XOneThirteenPellPowerSplit310101MazurTorsion.XOneThirteenDescent.PositivePellPowerSplitObstruction contract · MT-X13-NONCUSPMazurTorsion.XOneThirteenDescent.positive_pell_factor_power_split contract · MT-X13-NONCUSPMazurTorsion.XOneThirteenDescent.positive_pell_half_factors_isCoprime contract · MT-X13-NONCUSPMazurTorsion.XOneThirteenDescent.rationalPoint_addOrderOf_ne_thirteen_of_positivePellPowerSplit contract · MT-X13-NONCUSP
    MazurTorsion.NumberTheory.XOneThirteenPositivePell527271MazurTorsion.XOneThirteenDescent.PositivePellAllocatedFactorObstruction contract · MT-X13-NONCUSPMazurTorsion.XOneThirteenDescent.homogeneous_pell_identity contract · MT-X13-NONCUSPMazurTorsion.XOneThirteenDescent.odd_prime_pell_factor_allocation contract · MT-X13-NONCUSPMazurTorsion.XOneThirteenDescent.positive_split_rational_curve_point contract · MT-X13-NONCUSPMazurTorsion.XOneThirteenDescent.rationalPoint_addOrderOf_ne_thirteen_of_positivePellAllocatedFactor contract · MT-X13-NONCUSP
    MazurTorsion.NumberTheory.XZeroFortyNineTransfer815196MazurTorsion.XZeroFortyNine.rationalDatumOfSplitFiniteFlatSourceOfOrderFortyNineTorsion contract · MT-O49-TOWERMazurTorsion.XZeroFortyNine.rationalPoint_addOrderOf_ne_fortyNine_of_variableChangeClassifyingMap contract · MT-O49-TOWER
    MazurTorsion.PrimeOrder.CyclotomicObstruction248125MazurTorsion.PrimeOrder.divisionField_exists_nontrivial_p_torsion_capitulating_orbit contract · MT-CYCLOTOMIC-UNRAMIFIED
    MazurTorsion.PrimeOrder.FiniteFieldFive6333MazurTorsion.PrimeOrder.card_reductionAtFive_le_ten integrated · MT-PRIME-SHAFAREVICH
    MazurTorsion.PrimeOrder.FiniteFieldFiveOrder6231MazurTorsion.PrimeOrder.zmod_five_addOrderOf_ne_of_eleven_le integrated · MT-PRIME-SHAFAREVICH
    MazurTorsion.PrimeOrder.FormalImmersionAtFive14432MazurTorsion.PrimeOrder.valuation_j_le_one_of_formalImmersionAtFive contract · MT-PRIME-EISENSTEIN-SPECIALIZATION
    MazurTorsion.PrimeOrder.FormalImmersionNeronAtFive20262MazurTorsion.PrimeOrder.minimalCompletionAtFive_reduction_invariants_of_hasAdditiveReduction contract · MT-PRIME-HERBRAND-KUMMER
    MazurTorsion.PrimeOrder.FormalImmersionSpecialFiberAtFive31682MazurTorsion.PrimeOrder.rationalPoint_addOrderOf_ne_of_mappedCotangentAtFive_of_nonsingularReduction contract · MT-PRIME-EISENSTEIN-SPECIALIZATIONMazurTorsion.PrimeOrder.rationalPoint_addOrderOf_ne_of_mappedDegreeOneCotangentAtFive_of_nonsingularReduction contract · MT-PRIME-EISENSTEIN-SPECIALIZATIONMazurTorsion.PrimeOrder.rationalPoint_addOrderOf_ne_of_quotientCotangentAtFive_of_nonsingularReduction contract · MT-PRIME-EISENSTEIN-SPECIALIZATIONMazurTorsion.PrimeOrder.valuation_j_le_one_of_mappedIdealCotangentAtFive contract · MT-PRIME-EISENSTEIN-SPECIALIZATIONMazurTorsion.PrimeOrder.valuation_j_le_one_of_mappedIdealDegreeOneCotangentAtFive contract · MT-PRIME-EISENSTEIN-SPECIALIZATIONMazurTorsion.PrimeOrder.valuation_j_le_one_of_quotientCotangentCertificateAtFive contract · MT-PRIME-EISENSTEIN-SPECIALIZATION
    MazurTorsion.PrimeOrder.GoodReductionAtFive1,167414MazurTorsion.PrimeOrder.rationalPoint_addOrderOf_ne_of_eleven_le_of_goodReductionAtFive integrated · MT-PRIME-DIVISION-FIELDMazurTorsion.PrimeOrder.not_additiveReductionAtFive integrated · MT-PRIME-HERBRAND-KUMMERMazurTorsion.PrimeOrder.completionPoint_addOrderOf_ne_of_eleven_le_of_hasGoodReductionAtFive contract · MT-PRIME-SPLIT-SEQUENCEMazurTorsion.PrimeOrder.goodReductionAtFive integrated · MT-PRIME-SPLIT-SEQUENCE
    MazurTorsion.PrimeOrder.TameAdditiveAtFive943268MazurTorsion.PrimeOrder.addOrderOf_ne_prime_ge_eleven_of_componentExponentTwelveAtFive contract · MT-PRIME-HERBRAND-KUMMERMazurTorsion.PrimeOrder.addOrderOf_ne_prime_ge_eleven_of_nonsingularReduction_of_componentExponentTwelveAtFive contract · MT-PRIME-HERBRAND-KUMMERMazurTorsion.PrimeOrder.addOrderOf_ne_prime_ge_eleven_of_tameAdditiveFiltrationAtFive contract · MT-PRIME-HERBRAND-KUMMERMazurTorsion.PrimeOrder.tateAlgorithm_coefficientObstruction_of_hasAdditiveReduction contract · MT-PRIME-HERBRAND-KUMMERMazurTorsion.PrimeOrder.tateAlgorithm_hasAdditiveReduction_variableChange_of_valuation_u_eq_one contract · MT-PRIME-HERBRAND-KUMMERMazurTorsion.PrimeOrder.tateAlgorithm_translatedCoefficientObstruction_of_hasAdditiveReduction contract · MT-PRIME-HERBRAND-KUMMERMazurTorsion.PrimeOrder.tateAlgorithm_valuationInput_of_hasAdditiveReduction contract · MT-PRIME-HERBRAND-KUMMERMazurTorsion.PrimeOrder.hasGoodReduction_of_valuation_j_le_one_of_additiveOrderObstruction contract · MT-PRIME-SPLIT-SEQUENCEMazurTorsion.PrimeOrder.hasGoodReduction_of_valuation_j_le_one_of_tameAdditiveFiltrationAtFive contract · MT-PRIME-SPLIT-SEQUENCEMazurTorsion.PrimeOrder.not_hasMultiplicativeReduction_of_valuation_j_le_one contract · MT-PRIME-SPLIT-SEQUENCEMazurTorsion.PrimeOrder.valuation_j_gt_one_of_hasMultiplicativeReduction contract · MT-PRIME-SPLIT-SEQUENCE
    MazurTorsion.PrimeOrder.TorsionSpecialization197161MazurTorsion.PrimeOrder.specializedPointZMod_addOrderOf_eq_atFive_of_goodReduction integrated · MT-PRIME-DIVISION-FIELDMazurTorsion.PrimeOrder.specializedPoint_addOrderOf_eq_atFive_of_goodReduction integrated · MT-PRIME-DIVISION-FIELD
    MazurTorsion.Release.PinMigration4021MazurTheorem.Release.sharedDependencyGraph integrated · MT-PIN-MIGRATIONMazurTheorem.Release.tauCetiConsumerBuild integrated · MT-PIN-MIGRATION
    MazurTorsion.Upstream.AINTLIB.Picard.Pullback1,800907AlgebraicGeometry.Scheme.Pic.map contract · MT-TC-D1-PICARD-FUNCTOR
    MazurTorsion.Upstream.AINTLIB.Picard.RelativePic309192AlgebraicGeometry.Scheme.Modules.picRelFunctor contract · MT-TC-D1-PICARD-FUNCTORAlgebraicGeometry.Scheme.Modules.picRelFunctor_map_picRelProj contract · MT-TC-D1-PICARD-FUNCTOR
    MazurTorsion.Upstream.CurveCohomologyGrothendieckVanishing10044MazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.smoothProperCurve_H_eq_zero contract · MT-TC-B1-COHERENT-COHOMOLOGY
    MazurTorsion.Upstream.CurveDivisorDescent1,549655MazurTorsion.AlgebraicGeometry.CurveDivisorDescent.localLineBundleChosenOverlapHomOnProperSmoothCurve contract · MT-TC-A3-DIVISOR-LINE-BUNDLE
    MazurTorsion.Upstream.CurveLineBundleOverlapNaturality8431MazurTorsion.AlgebraicGeometry.LineBundleDescent.pullHom_pullbackOverlapHomOfModel contract · MT-TC-A3-DIVISOR-LINE-BUNDLEMazurTorsion.AlgebraicGeometry.LineBundleDescent.pullbackOverlapHomOfModel contract · MT-TC-A3-DIVISOR-LINE-BUNDLE
    MazurTorsion.Upstream.CurveLineBundleTripleIntersection29771MazurTorsion.AlgebraicGeometry.CurveDivisorDescent.tripleOverlapComparisonToIntersection contract · MT-TC-A3-DIVISOR-LINE-BUNDLEMazurTorsion.AlgebraicGeometry.CurveDivisorDescent.tripleOverlapComparisonToIntersection_comp_fromSpec contract · MT-TC-A3-DIVISOR-LINE-BUNDLE
    MazurTorsion.Upstream.ProjectiveLineCechHOneFinite1,920854MazurTorsion.AlgebraicGeometry.ProjectiveLineCohomology.genuineSheafHOne_finite_canonical_of_finite_to_projectiveLine contract · MT-TC-B1-COHERENT-COHOMOLOGY
    MazurTorsion.Upstream.ProperCurveCohomologyFinite383194MazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.genuineSheafHOneCanonical_finiteDimensional_of_rationalSection contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.genuineSheafHOne_finiteDimensional_of_rationalSection contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hOneCanonicalFieldLinearMap contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hOneCanonicalFieldModule contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hZeroCanonicalFieldLinearEquivGlobalSections contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hZeroCanonicalFieldModule contract · MT-TC-B1-COHERENT-COHOMOLOGY
    MazurTorsion.Upstream.SchemeModuleBaseCechHOneComparison18694MazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.nativeBaseCechHOneForgetIsoOfAffineOpenCover contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.nativeBaseCechHOneLinearEquivCanonicalOfAffineOpenCover contract · MT-TC-B1-COHERENT-COHOMOLOGY
    MazurTorsion.Upstream.SchemeModuleBaseCechHOneFinite9333MazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.genuineSheafHOne_finite_of_ordered_affineOpenCover contract · MT-TC-B1-COHERENT-COHOMOLOGY
    MazurTorsion.Upstream.SchemeModuleBaseCechHOneModule9062MazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.genuineSheafHOneLinearEquivNativeBaseCechOfAffineOpenCover contract · MT-TC-B1-COHERENT-COHOMOLOGY
    MazurTorsion.Upstream.SchemeModuleCohomologyAffine8852MazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.affineTildeHZeroEquiv contract · MT-TC-B1-COHERENT-COHOMOLOGY
    MazurTorsion.Upstream.SchemeModuleCohomologyHZero351255MazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.cohomologyLinearMap contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.globalSectionsCohomologyModule contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hZeroCanonicalLinearEquivGlobalSections contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hZeroEquivGlobalSections contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hZeroEquivGlobalSections_naturality contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hZeroModule contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.hZeroModule_eq_globalSectionsCohomologyModule contract · MT-TC-B1-COHERENT-COHOMOLOGYMazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.zariskiFunctor contract · MT-TC-B1-COHERENT-COHOMOLOGY
    456 supporting modules

    Checked support modules not named directly by a canonical ledger artifact.

    ModuleLinesDeclarationsImports
    EllipticCurves.Examples.ExceptionalCubicReduction182181
    EllipticCurves.IntegralModel11521
    EllipticCurves.Mathlib.AdicCompletionExtension377182
    EllipticCurves.Mathlib.AdicFormalGroupLog768422
    EllipticCurves.Mathlib.AdicValuation136101
    EllipticCurves.Mathlib.Basic1,6311491
    EllipticCurves.Mathlib.Chabauty.AdicTopology7262
    EllipticCurves.Mathlib.Chabauty.ExpConverge394263
    EllipticCurves.Mathlib.Chabauty.FormalGroupLaw.Basic314185
    EllipticCurves.Mathlib.Chabauty.FormalGroupLaw.Invariance670362
    EllipticCurves.Mathlib.Chabauty.FormalGroupLaw.Log377205
    EllipticCurves.Mathlib.Chabauty.FormalGroupLaw.Points19671
    EllipticCurves.Mathlib.Chabauty.FormalGroupLaw4004
    EllipticCurves.Mathlib.Chabauty.LocalRing4924
    EllipticCurves.Mathlib.Chabauty.LogIso553281
    EllipticCurves.Mathlib.Chabauty.MvPSeries536455
    EllipticCurves.Mathlib.Chabauty.MvPowerSeriesComp316287
    EllipticCurves.Mathlib.Chabauty.MvPowerSeriesPDeriv362204
    EllipticCurves.Mathlib.Chabauty.PSeries3243010
    EllipticCurves.Mathlib.Chabauty.PadicInt5722
    EllipticCurves.Mathlib.Chabauty.PadicValNat6733
    EllipticCurves.Mathlib.EllipticCurvePoint148151
    EllipticCurves.ReductionAtPrime467323
    EllipticCurves.VariableChange2001
    EllipticCurves.WeierstrassFormalGroup.Chord1,025833
    EllipticCurves.WeierstrassFormalGroup.Eval621551
    EllipticCurves.WeierstrassFormalGroup.Filtration969374
    EllipticCurves.WeierstrassFormalGroup.Foundations891552
    EllipticCurves.WeierstrassFormalGroup.GroupLaw961273
    EllipticCurves.WeierstrassFormalGroup.Reduction800503
    EllipticCurves.WeierstrassFormalGroup.ThirdPoint704402
    EllipticCurves53031
    MazurTorsion.Algebra.HopfLocalizationAway343252
    MazurTorsion.AlgebraicGeometry.FiniteEtaleRelativeDimensionDescent22848
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.AdditiveFppfHOneField672594
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleClosedFiberConnectedEtale425246
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleClosedFiberConnectedEtaleConsumers9541
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.AdmissibleClosedFiberFactorIdentification363174
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ArtinSchreierAdmissiblePrimeFiberConsumers340192
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ArtinSchreierConstantKernel8395111
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ArtinSchreierFppfHOne206186
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ArtinSchreierIntegralClosedFiberHOneConsumers313151
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ArtinSchreierMapFppf392386
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemeFppfConnecting856522
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemeFppfMiddleExact357131
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemeFppfQuotient341282
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemeKernel301271
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemeKernelPresentation673531
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemePowerKummerRankZero22082
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ConnectedEtale204134
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.Constant1,001733
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantFlat497469
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantFlatBadFiberClosedFiberConsumers193122
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantFlatBadFiberClosedFiberControl905573
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantFlatBadFiberHZero283235
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantFlatGlobalHOneLocalization11462
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantFlatGlobalSections17982
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ConstantSections739325
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.ElementaryGlobalSections219141
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.Examples290224
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FiniteTranslationQuotientGroup1,9591192
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfCardinalityBound13191
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfConnecting382562
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfHOneBaseIso793564
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfHOneCommGroup615501
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfHOneShortExactInjective34565
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfHOneUniverse281282
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfKummerInjectionFromExactMultiplication611325
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfQuotientBoundaryInjection131101
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfQuotientConnecting1,016474
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.FppfQuotientEuler9511
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.KummerLocalizationAway395249
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MuKernelPrimeFiberKummerRankZero396235
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MuSchemePowerKernelComparison515294
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeBadFiberKummerHOne179136
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeCocycleDescent1,060825
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeFiniteAffineFamily260266
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeFiniteAffineFamilyEffectivity991808
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeFlat9238311
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeFlatGlobalSections14882
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeFppfHOneField264131
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeIntegralHOneRankZeroConsumers15963
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativeKummer516464
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativePowerFppfBoundaryConsumers159132
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.MultiplicativePowerMapFppf400242
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.Operations11191
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.QuasiFiniteBadLevelEuler379155
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.QuasiFiniteBadLevelKummerRankZero344132
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.QuasiFiniteFppfConnecting279342
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.QuasiFiniteFppfHOne152163
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.QuasiFiniteFppfQuotientEuler22653
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.QuasiFiniteKernelPresentation284241
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.QuasiFiniteQuotient11682
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.SupportedFppfCokernel365427
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.SupportedFppfHOne15383
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.SupportedFppfHOneBridge32982
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.SupportedFppfHOneCertifiedData13062
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.SupportedFppfLocalization349352
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.SupportedFppfSerre13262
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.SupportedFppfSerreQuotient160132
    MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.SupportedPointCokernel331287
    MazurTorsion.AlgebraicGeometry.FormalImmersion268164
    MazurTorsion.AlgebraicGeometry.FormalImmersionAffineFiber958452
    MazurTorsion.AlgebraicGeometry.FormalImmersionAffineFiberSpec326132
    MazurTorsion.AlgebraicGeometry.FormalImmersionCollision21993
    MazurTorsion.AlgebraicGeometry.FormalImmersionIdentity6341
    MazurTorsion.AlgebraicGeometry.FormalImmersionNakayama379175
    MazurTorsion.AlgebraicGeometry.NeronModel.PowerKummerRankZero6812
    MazurTorsion.AlgebraicGeometry.PicardSectionBaseChange10051
    MazurTorsion.AlgebraicGeometry.ReducedClosedSubscheme6943
    MazurTorsion.AlgebraicGeometry.SchemeModuleCohomology.LocalKilling911426
    MazurTorsion.AlgebraicGeometry.SmoothCurveRationalSection12923
    MazurTorsion.AlgebraicGeometry.XOneThirteenAffineCurve207242
    MazurTorsion.AlgebraicGeometry.XOneThirteenCohomology5922
    MazurTorsion.AlgebraicGeometry.XOneThirteenFiniteFieldCurve118102
    MazurTorsion.AlgebraicGeometry.XOneThirteenHyperellipticMap1,757983
    MazurTorsion.AlgebraicGeometry.XOneThirteenProjectiveCurve772664
    MazurTorsion.AlgebraicGeometry.XOneThirteenProjectiveFiniteFieldCurve789715
    MazurTorsion.AlgebraicGeometry.XOneThirteenProjectivePoints288321
    MazurTorsion.Arithmetic.ExceptionalProducts10295
    MazurTorsion.Arithmetic.ExceptionalTwoTen4852011
    MazurTorsion.Arithmetic.ExceptionalTwoTwelve402132
    MazurTorsion.Arithmetic.LowTorsionObstructions7485
    MazurTorsion.Arithmetic.OddPrimeObstructions9185
    MazurTorsion.Arithmetic.OrderTwentyTwentyFour13153
    MazurTorsion.Arithmetic.PointOrderReduction14776
    MazurTorsion.EllipticCurve.CuspidalReduction284134
    MazurTorsion.EllipticCurve.DoublingCoordinates228152
    MazurTorsion.EllipticCurve.IntegerPrimeSpecialization222261
    MazurTorsion.EllipticCurve.MinimalModelScaling24692
    MazurTorsion.EllipticCurve.NonsingularReductionAdditive887341
    MazurTorsion.EllipticCurve.NonsingularReductionVariableChange30261
    MazurTorsion.EllipticCurve.TameAdditiveFiltration27093
    MazurTorsion.EllipticCurve.TateFirstBlowup416267
    MazurTorsion.EllipticCurve.TateResidueTranslation169102
    MazurTorsion.EllipticCurve.TateShortCoefficientDepth203105
    MazurTorsion.EllipticCurve.TateStarDepthFour55431
    MazurTorsion.EllipticCurve.TateStarDepthSix54552
    MazurTorsion.EllipticCurve.TateStarRepeatedRoot40241
    MazurTorsion.EllipticCurve.TateStarSimpleRoot58762
    MazurTorsion.EllipticCurve.TateTypeIIComponent15542
    MazurTorsion.EllipticCurve.TateTypeIIIComponent32921
    MazurTorsion.EllipticCurve.TateTypeIVComponent51121
    MazurTorsion.EllipticCurve.TwoIsogeny690513
    MazurTorsion.EllipticCurve.TwoIsogenyMultiples523162
    MazurTorsion.EllipticCurve.TwoTorsionNormalization238152
    MazurTorsion.EllipticCurve.VariableChange268203
    MazurTorsion.EllipticCurve.VeluPair144123
    MazurTorsion.Foundations.DivisionPolynomialDiscriminantFive639543
    MazurTorsion.Foundations.DivisionPolynomialDiscriminantSeven1,053683
    MazurTorsion.Foundations.DivisionPolynomialRootCriterion656126
    MazurTorsion.Foundations.FullFourTorsion37366
    MazurTorsion.Foundations.OddPrimeFullTorsion480217
    MazurTorsion.Foundations.Polynomial.BoundedResultant36083
    MazurTorsion.Foundations.ThreeTorsion536115
    MazurTorsion.Foundations.TwoTorsion241128
    MazurTorsion.GroupTheory.CyclicKernelExtension9613
    MazurTorsion.GroupTheory.ForbiddenEmbeddings7571
    MazurTorsion.GroupTheory.IndependentCyclicGenerators224104
    MazurTorsion.GroupTheory.IndexNSmulFG16173
    MazurTorsion.GroupTheory.TorsionEquiv6051
    MazurTorsion.Kubert.OrderEighteenModel343181
    MazurTorsion.Kubert.OrderEighteenReduction13832
    MazurTorsion.Kubert.OrderElevenModel384261
    MazurTorsion.Kubert.OrderElevenReduction346121
    MazurTorsion.Kubert.OrderFifteen4822
    MazurTorsion.Kubert.OrderFifteenModel472292
    MazurTorsion.Kubert.OrderFifteenReduction22082
    MazurTorsion.Kubert.OrderFourteen5122
    MazurTorsion.Kubert.OrderFourteenModel466362
    MazurTorsion.Kubert.OrderFourteenReduction551221
    MazurTorsion.Kubert.OrderNineReduction19651
    MazurTorsion.Kubert.OrderSixteenReduction1,090293
    MazurTorsion.Kubert.OrderThirteenModel14191
    MazurTorsion.Kubert.OrderThirteenReduction452131
    MazurTorsion.Kubert.OrderThirtyFive551175
    MazurTorsion.Kubert.OrderThirtyFiveCuspidalReductionAtEleven13552
    MazurTorsion.Kubert.OrderThirtyFiveFormalImmersionAtEleven380103
    MazurTorsion.Kubert.OrderThirtyFiveGoodReductionAtEleven1,175412
    MazurTorsion.Kubert.OrderTwentyOne8933
    MazurTorsion.Kubert.OrderTwentyOneExceptionalJ185102
    MazurTorsion.Kubert.OrderTwentyOneReduction18133
    MazurTorsion.Kubert.OrderTwentySevenEndpoint10061
    MazurTorsion.Kubert.OrderTwentySevenLegs104111
    MazurTorsion.Kubert.OrderTwentySevenReduction17952
    MazurTorsion.Kubert.OrderTwentySevenTrisection374113
    MazurTorsion.Kubert.TateNormalForm376146
    MazurTorsion.Kubert.ThreeNormalForm222111
    MazurTorsion.ModularCurve.AffineCuspArithmeticConsumers1,210163
    MazurTorsion.ModularCurve.AffineCuspChartTransport493301
    MazurTorsion.ModularCurve.AffineCuspPicardSectionBaseChange124112
    MazurTorsion.ModularCurve.AffineCuspQExpansion461103
    MazurTorsion.ModularCurve.AffineCuspResidueRetraction638231
    MazurTorsion.ModularCurve.CompleteDVRStalk782284
    MazurTorsion.ModularCurve.DegreeOneCotangent209132
    MazurTorsion.ModularCurve.OrderThirtyFiveInfinityChartFirstOrder8742
    MazurTorsion.ModularCurve.XZeroEllipticQuotientAtlas138114
    MazurTorsion.ModularCurve.XZeroEllipticQuotientRepresentability978686
    MazurTorsion.ModularCurve.XZeroEllipticQuotientTranslation15264
    MazurTorsion.ModularCurve.XZeroFiniteFlatClassifyingData244121
    MazurTorsion.ModularCurve.XZeroFiniteFlatCyclicQuotient348262
    MazurTorsion.ModularCurve.XZeroFiniteFlatModuli761574
    MazurTorsion.ModularCurve.XZeroGeometricCyclicQuotient10862
    MazurTorsion.ModularCurve.XZeroThirtyFive132151
    MazurTorsion.ModularCurve.XZeroWeierstrassAbelianVariety161113
    MazurTorsion.ModularCurve.XZeroWeierstrassAbelianVarietyTransfer15251
    MazurTorsion.ModularCurve.XZeroWeierstrassAntidiagonalAddition563271
    MazurTorsion.ModularCurve.XZeroWeierstrassCubicBaseChange373231
    MazurTorsion.ModularCurve.XZeroWeierstrassCubicChartDensity378211
    MazurTorsion.ModularCurve.XZeroWeierstrassCubicReducedBaseChange836743
    MazurTorsion.ModularCurve.XZeroWeierstrassGeometricIntegrality653573
    MazurTorsion.ModularCurve.XZeroWeierstrassProjectiveCubic879788
    MazurTorsion.ModularCurve.XZeroWeierstrassProjectiveInfinity10651
    MazurTorsion.ModularCurve.XZeroWeierstrassProjectiveNegation290272
    MazurTorsion.ModularCurve.XZeroWeierstrassProjectivePlaneBaseChange774584
    MazurTorsion.ModularCurve.XZeroWeierstrassProjectivePointComparison490181
    MazurTorsion.ModularCurve.XZeroWeierstrassProjectivePointInverse353171
    MazurTorsion.ModularCurve.XZeroWeierstrassProjectivePointNegation190102
    MazurTorsion.ModularCurve.XZeroWeierstrassRelativeDimension366194
    MazurTorsion.ModularCurve.XZeroWeierstrassSecantAddition805814
    MazurTorsion.ModularCurve.XZeroWeierstrassTangentAddition366333
    MazurTorsion.ModularCurve.XZeroWeierstrassVerticalAddition619301
    MazurTorsion.NumberTheory.CyclotomicHilbert948022
    MazurTorsion.NumberTheory.CyclotomicJacobiCharacter536336
    MazurTorsion.NumberTheory.CyclotomicJacobiIdealFaithful476222
    MazurTorsion.NumberTheory.CyclotomicJacobiReciprocityReduction23864
    MazurTorsion.NumberTheory.CyclotomicJacobiSumTwo297133
    MazurTorsion.NumberTheory.CyclotomicKummer1,683736
    MazurTorsion.NumberTheory.CyclotomicKummerFrobeniusCoordinate10871
    MazurTorsion.NumberTheory.CyclotomicKummerResidueAlgebra204111
    MazurTorsion.NumberTheory.CyclotomicKummerResidueCovariance362142
    MazurTorsion.NumberTheory.CyclotomicKummerResidueProduct540183
    MazurTorsion.NumberTheory.CyclotomicKummerResidueSymbol530222
    MazurTorsion.NumberTheory.CyclotomicLocalPrimaryCongruence21342
    MazurTorsion.NumberTheory.CyclotomicNormalizedLocalPrimary6012
    MazurTorsion.NumberTheory.CyclotomicNormalizedResidueWeight25071
    MazurTorsion.NumberTheory.CyclotomicOrbitCoprimeNormalization13141
    MazurTorsion.NumberTheory.CyclotomicPseudoUnitNormalization25621
    MazurTorsion.NumberTheory.CyclotomicPseudoUnitReciprocity20071
    MazurTorsion.NumberTheory.CyclotomicPseudoUnitUnramified42543
    MazurTorsion.NumberTheory.CyclotomicResidueOrbitFaithful11731
    MazurTorsion.NumberTheory.CyclotomicSelmerClassGroup19582
    MazurTorsion.NumberTheory.CyclotomicStickelbergerTwo200113
    MazurTorsion.NumberTheory.CyclotomicStickelbergerTwoResidue355183
    MazurTorsion.NumberTheory.CyclotomicUnramified1,134718
    MazurTorsion.NumberTheory.ExceptionalCubicDescent1,1845610
    MazurTorsion.NumberTheory.ExceptionalCubicReduction4222
    MazurTorsion.NumberTheory.ExceptionalQuarticDescent511103
    MazurTorsion.NumberTheory.FermatCubicClassification10521
    MazurTorsion.NumberTheory.KummerArtinProduct547222
    MazurTorsion.NumberTheory.OrderThirtyFiveAbelianVarietyTransfer3612
    MazurTorsion.NumberTheory.OrderThirtyFiveEisensteinDescent798403
    MazurTorsion.NumberTheory.OrderThirtyFiveEisensteinIdealSupport619301
    MazurTorsion.NumberTheory.OrderThirtyFiveInfinityChartScheme352503
    MazurTorsion.NumberTheory.OrderThirtyFiveQuotient172182
    MazurTorsion.NumberTheory.OrderThirtyFiveQuotientMap245221
    MazurTorsion.NumberTheory.OrderThirtyFiveQuotientReduction311193
    MazurTorsion.NumberTheory.OrderThirtyFiveQuotientScheme272362
    MazurTorsion.NumberTheory.OrderThirtyFiveRankBoundary251164
    MazurTorsion.NumberTheory.OrderThirtyFiveTargetCubic530371
    MazurTorsion.NumberTheory.OrderThirtyFiveThreeDescent865282
    MazurTorsion.NumberTheory.OrderThirtyFiveThreeIsogeny408263
    MazurTorsion.NumberTheory.OrderThirtyFiveThreeIsogenyDual696471
    MazurTorsion.NumberTheory.QuarticDifferenceDescent340131
    MazurTorsion.NumberTheory.RationalRootsOfUnity4122
    MazurTorsion.NumberTheory.SelmerClassGroup1,034632
    MazurTorsion.NumberTheory.SevenAdicCertificates11966
    MazurTorsion.NumberTheory.UnramifiedArtin711468
    MazurTorsion.NumberTheory.UnramifiedNormArtin27892
    MazurTorsion.NumberTheory.WeakChebotarev783355
    MazurTorsion.NumberTheory.XOneEighteenCubeCorrespondence16691
    MazurTorsion.NumberTheory.XOneEighteenDescent1,577942
    MazurTorsion.NumberTheory.XOneEighteenEisensteinAllocation1,538684
    MazurTorsion.NumberTheory.XOneEighteenFiniteField429523
    MazurTorsion.NumberTheory.XOneEighteenQuadraticNormParametrization496131
    MazurTorsion.NumberTheory.XOneElevenDescent551354
    MazurTorsion.NumberTheory.XOneElevenFiveIsogeny1,150713
    MazurTorsion.NumberTheory.XOneElevenReduction321302
    MazurTorsion.NumberTheory.XOneFifteenDescent1,530661
    MazurTorsion.NumberTheory.XOneFifteenReduction559383
    MazurTorsion.NumberTheory.XOneFourteenDescent1,145571
    MazurTorsion.NumberTheory.XOneFourteenReduction224172
    MazurTorsion.NumberTheory.XOneThirteenDescent2,1271353
    MazurTorsion.NumberTheory.XOneThirteenFiniteField1,0711443
    MazurTorsion.NumberTheory.XZeroFortyNineDescent1,306515
    MazurTorsion.NumberTheory.XZeroFortyNineEllipticQuotient390273
    MazurTorsion.NumberTheory.XZeroFortyNineEtaModel156141
    MazurTorsion.NumberTheory.XZeroFortyNineLevelSevenQuotient17592
    MazurTorsion.NumberTheory.XZeroFortyNineReduction233152
    MazurTorsion.NumberTheory.XZeroTwentyOneDescent7603718
    MazurTorsion.NumberTheory.XZeroTwentyOneRankZero1,236596
    MazurTorsion.NumberTheory.XZeroTwentyOneReduction413232
    MazurTorsion.NumberTheory.XZeroTwentyOneTransfer577142
    MazurTorsion.NumberTheory.XZeroTwentySevenClassification1,443833
    MazurTorsion.PrimeOrder.CuspidalReductionAtFive14152
    MazurTorsion.Release.PinMigrationAudit2921
    MazurTorsion.Upstream.AINTLIB.FltRegular.NumberTheory.CyclotomicRing123162
    MazurTorsion.Upstream.AINTLIB.FltRegular.NumberTheory.Hilbert92794477
    MazurTorsion.Upstream.AINTLIB.FltRegular.NumberTheory.Hilbert9422379
    MazurTorsion.Upstream.AINTLIB.FltRegular.NumberTheory.RegularPrimes3011
    MazurTorsion.Upstream.AINTLIB.FltRegular.NumberTheory.SystemOfUnits11071
    MazurTorsion.Upstream.AINTLIB.FltRegular.NumberTheory.Unramified21956
    MazurTorsion.Upstream.AINTLIB.ForMathlib.AcyclicAffineCechComparison6832
    MazurTorsion.Upstream.AINTLIB.ForMathlib.AdjunctionUnitIsoTransport8731
    MazurTorsion.Upstream.AINTLIB.ForMathlib.AffineIdealQuotientPullbackUnit16253
    MazurTorsion.Upstream.AINTLIB.ForMathlib.AffineModuleBaseChange286102
    MazurTorsion.Upstream.AINTLIB.ForMathlib.AffineQuotient1,333356
    MazurTorsion.Upstream.AINTLIB.ForMathlib.BaseChangeAlongCompat1682713
    MazurTorsion.Upstream.AINTLIB.ForMathlib.CartierDual753479
    MazurTorsion.Upstream.AINTLIB.ForMathlib.EtaleCancellation18077
    MazurTorsion.Upstream.AINTLIB.ForMathlib.FiniteAffineSupportAnnihilation19574
    MazurTorsion.Upstream.AINTLIB.ForMathlib.FiniteFamilySupportAnnihilation9041
    MazurTorsion.Upstream.AINTLIB.ForMathlib.FiniteHomologySequence9863
    MazurTorsion.Upstream.AINTLIB.ForMathlib.FiniteModuleSupportAnnihilation5634
    MazurTorsion.Upstream.AINTLIB.ForMathlib.FinitePresentationOfFinite3911
    MazurTorsion.Upstream.AINTLIB.ForMathlib.FiniteSupportIdealSheafPullbackUnit7315
    MazurTorsion.Upstream.AINTLIB.ForMathlib.FormalCoproductAdditive4812
    MazurTorsion.Upstream.AINTLIB.ForMathlib.IdealSheafAffineChartPullbackUnit8523
    MazurTorsion.Upstream.AINTLIB.ForMathlib.IdealSheafPowerSubscheme4832
    MazurTorsion.Upstream.AINTLIB.ForMathlib.IdealSheafSubschemeAffineChart8352
    MazurTorsion.Upstream.AINTLIB.ForMathlib.IdealSheafSubschemeRestrictPullbackUnit5912
    MazurTorsion.Upstream.AINTLIB.ForMathlib.InvariantBaseChange285225
    MazurTorsion.Upstream.AINTLIB.ForMathlib.InvariantLocalization213132
    MazurTorsion.Upstream.AINTLIB.ForMathlib.InvariantTorsor1,126415
    MazurTorsion.Upstream.AINTLIB.ForMathlib.PresheafPullbackCompMonoidal12911
    MazurTorsion.Upstream.AINTLIB.ForMathlib.PullbackCompMonoidal1,3571122
    MazurTorsion.Upstream.AINTLIB.ForMathlib.PullbackLocalAtTarget12633
    MazurTorsion.Upstream.AINTLIB.ForMathlib.QuotientTorsor26552
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeActionFree487157
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeInducingOpenLift6751
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleBaseCech484234
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleBaseCechBasic305214
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleBaseCechExact22878
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleBaseCechHomology19063
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleBaseCechPushforward18261
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleCanonicalSupportFull7521
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleCanonicalSupportThickening116111
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleClosedStalkSupport6564
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleComparisonCoherent7212
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleComparisonSupport17272
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOpenCoverIso11623
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOpenUnitIso469241
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechAlternating1,142483
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechBasic315223
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechComparison319232
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechExact15542
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechFunctor177101
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechHOne48883
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechHOneFinite7721
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechHomologyRetract5011
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechLowDegreeFinite28163
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleOrderedBaseCechPushforward429161
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModulePullbackUnitComposition11042
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModulePushforwardMapRestrictionIso6911
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModulePushforwardPullbackSupport8923
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleQuasicoherent1,9727114
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleRestrictLimits6732
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleRestrictPushforward12931
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleRestrictionIsoMonotone5512
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleSheaf9853
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleSupport334196
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeModuleSupportDrop8241
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SchemeQuotient1,8931122
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechCochains11096
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechDifferential16461
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechFlasqueHOne16981
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechGlobalSections396132
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechInjectiveAugmentation639345
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechInjectiveBicomplex125113
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechInjectiveComparison494291
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechSheafAugmentation11671
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechSheafComplex8661
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechSheafDifferential225132
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechSheafLocalContraction174121
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechSheafPositiveExact11732
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechSheafResolution5731
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechSheafTerms280162
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCechSheafZeroExact283151
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCohomologyCompat6763
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafCohomologyExact184162
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafDerivedGlobalSections737405
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafModuleFiniteTypeQuotient6413
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SheafOfModulesMonoidal714323
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SpecBasicOpen2011
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SpecGroupAction150102
    MazurTorsion.Upstream.AINTLIB.ForMathlib.SurjectiveRestrictionScalars5022
    MazurTorsion.Upstream.AINTLIB.ForMathlib.TopCatSheafRestrict117122
    MazurTorsion.Upstream.AINTLIB.ForMathlib.TorsorMap365134
    MazurTorsion.Upstream.AINTLIB.ForMathlib.TotalComplexUpNat7241
    MazurTorsion.Upstream.AINTLIB.ForMathlib.TotalComplexUpNatHorizontalEdge7521
    MazurTorsion.Upstream.AINTLIB.ForMathlib.TotalComplexUpNatHorizontalEdgeHOne511253
    MazurTorsion.Upstream.AINTLIB.ForMathlib.TotalComplexUpNatLowDegrees11061
    MazurTorsion.Upstream.AINTLIB.ForMathlib.TotalComplexUpNatVerticalEdge9331
    MazurTorsion.Upstream.AINTLIB.Picard.Pic12754
    MazurTorsion.Upstream.AINTLIB.Picard.PullbackTensorSection836311
    MazurTorsion.Upstream.AffineDivisorLocalization4,4552038
    MazurTorsion.Upstream.AffineDivisorTensorAdd14971
    MazurTorsion.Upstream.AffineDivisorTensorBaseChange22571
    MazurTorsion.Upstream.AffineDivisorTildeTensorBaseChange1,673473
    MazurTorsion.Upstream.AffineDivisorTildeTensorOverlapNaturality17641
    MazurTorsion.Upstream.AffineDivisorTildeTensorPullbackSection35582
    MazurTorsion.Upstream.AffineDivisorTildeTensorRestrictionOverlapNaturality19522
    MazurTorsion.Upstream.AffineTildeReflectsInvertibility396146
    MazurTorsion.Upstream.AffineTildeTensorNaturality398211
    MazurTorsion.Upstream.AffineTildeTensorPullbackCoherence801213
    MazurTorsion.Upstream.CurveAffineChart1,112649
    MazurTorsion.Upstream.CurveDivisorPicardDescent1,449611
    MazurTorsion.Upstream.CurveDivisorRationalBoundary271111
    MazurTorsion.Upstream.CurveDivisorTensorAddChosenOverlap1,539482
    MazurTorsion.Upstream.CurveDivisorTensorAddDescent19381
    MazurTorsion.Upstream.CurveDivisorTensorAddFactorwiseChosenOverlap372142
    MazurTorsion.Upstream.CurveDivisorTensorAddFactorwiseDescent11832
    MazurTorsion.Upstream.CurveDivisorTensorAddOverlap938142
    MazurTorsion.Upstream.CurveDivisorTensorAddRestriction9712
    MazurTorsion.Upstream.CurveDivisorTensorAddTildeRestriction36262
    MazurTorsion.Upstream.CurveLineBundleCocycleForcesNormalization10031
    MazurTorsion.Upstream.CurveLineBundleCompatibleFamilies2,388762
    MazurTorsion.Upstream.CurveLineBundleDescent1,090745
    MazurTorsion.Upstream.CurveLineBundleLocality250192
    MazurTorsion.Upstream.CurveLineBundleNamedTripleCocycle705271
    MazurTorsion.Upstream.CurveLineBundleNormalizedTransition12041
    MazurTorsion.Upstream.CurveLineBundleRawCocycleComparisons17531
    MazurTorsion.Upstream.CurveLineBundleRawCocyclePrime28962
    MazurTorsion.Upstream.CurveLineBundleTransitionCocycle970161
    MazurTorsion.Upstream.CurveLineBundleTripleNaturality43772
    MazurTorsion.Upstream.CurveLineBundleTripleProjectionCocycle35581
    MazurTorsion.Upstream.CurveLineBundleTripleTower41561
    MazurTorsion.Upstream.DivisorLineBundle1,9111587
    MazurTorsion.Upstream.Geometry52029
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.ClosedImmersion5402318
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.ClosedImmersionCohomology13723
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.CohomologyAPI785458
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.ConstantSheafFlasque26083
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.FinitelyGeneratedVanishing42293
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.FlasqueVanishing431173
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.GeneratedSubsheaf233141
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.GrothendieckVanishing14841
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.GrothendieckVanishingOverview1803
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.IrreducibleStep630127
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.PresheafFilteredColimit738201
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.PresheafFilteredColimitCore600343
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.PresheafFilteredColimitGeneral414101
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.TopologicalKrullDim285185
    MazurTorsion.Upstream.LeanPool.GrothendieckVanishing.ZeroOutside557271
    MazurTorsion.Upstream.SchemeModuleCohomologyAffineCover184115
    MazurTorsion.Upstream.SchemeModuleCohomologyAffineCoverMono11232
    MazurTorsion.Upstream.SchemeModuleCohomologyAffineExact14153
    MazurTorsion.Upstream.SchemeModuleCohomologyAffineHOne7632
    MazurTorsion.Upstream.SchemeModuleCohomologyAffineHThree548293
    MazurTorsion.Upstream.SchemeModuleCohomologyAffineHTwo354163
    MazurTorsion.Upstream.SchemeModuleCohomologyAffineLocalKilling1601
    MazurTorsion.Upstream.SchemeModuleCohomologyDimensionShift9333
    MazurTorsion.Upstream.SchemeModuleFinitePushforward5422
    MazurTorsion.Upstream.SchemeModuleFinitePushforwardCech9623
    MazurTorsion.Upstream.SchemeModuleOrderedBaseCechLowDegreeSupport11251
    MazurTorsion3000273
    1,342 cache-heavy certificate modules

    The existing cache policy assigns these internals to the specialized generated-proof partition. They are collapsed only in this human view; every module, path, import, and declaration remains in the JSON index.

    Cache-heavy familyModulesLinesDeclarationsImports
    MazurTorsion.Kubert.OrderSeven*1,2551,526,78963,7295,788
    MazurTorsion.Kubert.OrderTwentyFive*59866412
    MazurTorsion.Kubert.OrderTwentySeven*8243,5802,207432