Mazur's rational torsion theorem

Blueprint Summary🔗

Overview
Total entries48completed: 0; deps incomplete: 0; sorries: 0; no proof: 32
Ready now1Entries with an actionable next formalization step.
Fully closed0Local code and prerequisite closure are both complete.
Actionable priorities1Entries ready now and already unlocking downstream work.
Actionable priorities (1)
  • «MT-BASE-INTEGRATED»(Theorem)
    Ready for proof work.
    effort: largepriority: hightag: milestonetag: donetag: integratedtag: mazurstage: proofstatement: ready to formalizedirect uses: 13downstream unlocks: 47proof: ready to formalize
Entry index (48)
Definitions16completed: 0; deps incomplete: 0; sorries: 0; no proof: 0
Theorems32completed: 0; deps incomplete: 0; sorries: 0; no proof: 32
Informal-only entries48
Definition Index (16)
Theorem / Proposition / Lemma / Corollary Index (32)
By parent groups (5)
Néron models, finite-flat group schemes, integral modular curves, Hecke operators, and the Eisenstein quotient. Stage weight: 400 points. (5)
Pin convergence, stable APIs, final assembly, kernel audit, and exposition. Stage weight: 50 points. (4)
Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points. (6)
Close orders 18, 25, 35, and 49 and the separate prime levels 11 and 13. Stage weight: 100 points. (8)
The specialization, unramified-extension, splitting, and isogeny-chain argument for primes at least 17. Stage weight: 100 points. (8)
Dependency insights
Statement-used entries47Entries reused in statement dependencies.
Tracked parent groups5Grouped health rollups for parents with more than one child entry.
Most used in statements (47)
  • «MT-BASE-INTEGRATED»(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 47
  • «MT-TC-E1-JACOBIAN-VARIETY»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 19
  • «MT-EC-ISOGENY-WEIL»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 17
  • «MT-TC-A3-DIVISOR-LINE-BUNDLE»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 26
  • «MT-TC-C1-RELATIVE-COHOMOLOGY»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 23
  • «MT-TC-B1-COHERENT-COHOMOLOGY»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 25
  • «MT-X0-INTEGRAL»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 13
  • «MT-FFGS-OORT-RAYNAUD»(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
  • «MT-NERON-SPECIALIZATION»(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 11
  • «MT-TC-A1-ORDER-SUPPORT»(Theorem)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 28
  • Show all 37 more statement-used entries
    • «MT-TC-A2-PRODUCT-FORMULA»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 27
    • «MT-TC-B2-RR-SERRE»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 21
    • «MT-TC-C2-SYMMETRIC-POWERS»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 21
    • «MT-TC-D1-PICARD-FUNCTOR»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 21
    • «MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
    • «MT-TC-E0-PRODUCT-DIM»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
    • «MT-X0-MODULI»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
    • «MT-FFGS-BASIC»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
    • «MT-NERON-BASE»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
    • «MT-FFGS-CONNECTED-ETALE»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
    • «MT-NERON-COMPONENTS»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
    • «MT-TC-F1-ABEL-JACOBI»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
    • «MT-X0-JACOBIAN»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
    • «MT-X0-HECKE»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
    • «MT-PRIME-SEMISTABLE»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
    • «MT-X0-CUSPS»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
    • «MT-X0-EISENSTEIN-ALGEBRA»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
    • «MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
    • «MT-X0-EISENSTEIN-QUOTIENT»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
    • «MT-CYCLOTOMIC-UNRAMIFIED»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
    • «MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
    • «MT-PRIME-DIVISION-FIELD»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
    • «MT-PRIME-HERBRAND-KUMMER»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
    • «MT-X11-COSET»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
    • «MT-O25-EXCLUDE»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «MT-O35-EXCLUDE»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «MT-O49-TOWER»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «MT-PRIME-SHAFAREVICH»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «MT-PRIME-SPLIT-SEQUENCE»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «MT-X11-JOIN»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «MT-X13-NONCUSP»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «MT-X18-NONCUSP»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «MT-FINITE-JOIN»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «MT-PIN-MIGRATION»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «MT-PRIME-ISOGENY-CHAIN»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «MT-API-INTEGRATION»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «MT-FINAL-ASSEMBLY»(Theorem)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Group health (5)
  • Reusable divisor, cohomology, Picard, Jacobian, Abel–Jacobi, and isogeny infrastructure, developed upstream where possible. Stage weight: 300 points.shared_geometry
    Grouped view over entries sharing the same parent.
    total: 13closed: 0local-only: 0ready: 0blocked: 13incomplete Lean: 0unlock score: 280
    Next: no ready child currently unlocks downstream work.
  • Néron models, finite-flat group schemes, integral modular curves, Hecke operators, and the Eisenstein quotient. Stage weight: 400 points.prime_infrastructure
    Grouped view over entries sharing the same parent.
    total: 14closed: 0local-only: 0ready: 0blocked: 14incomplete Lean: 0unlock score: 153
    Next: no ready child currently unlocks downstream work.
  • The specialization, unramified-extension, splitting, and isogeny-chain argument for primes at least 17. Stage weight: 100 points.prime_argument
    Grouped view over entries sharing the same parent.
    total: 8closed: 0local-only: 0ready: 0blocked: 8incomplete Lean: 0unlock score: 46
    Next: no ready child currently unlocks downstream work.
  • Close orders 18, 25, 35, and 49 and the separate prime levels 11 and 13. Stage weight: 100 points.finite_endpoints
    Grouped view over entries sharing the same parent.
    total: 8closed: 0local-only: 0ready: 0blocked: 8incomplete Lean: 0unlock score: 32
    Next: no ready child currently unlocks downstream work.
  • Pin convergence, stable APIs, final assembly, kernel audit, and exposition. Stage weight: 50 points.integration
    Grouped view over entries sharing the same parent.
    total: 4closed: 0local-only: 0ready: 0blocked: 4incomplete Lean: 0unlock score: 6
    Next: no ready child currently unlocks downstream work.
Metadata
Tags in use26Distinct tags currently attached to blueprint entries.
Tag rollups (26)
  • tag: mazur
    entries: 11actionable: 1quick wins: 0linked PRs: 0
  • tag: done
    entries: 1actionable: 1quick wins: 0linked PRs: 0
  • tag: integrated
    entries: 1actionable: 1quick wins: 0linked PRs: 0
  • tag: milestone
    entries: 1actionable: 1quick wins: 0linked PRs: 0
  • tag: blocked
    entries: 34actionable: 0quick wins: 0linked PRs: 0
  • tag: nouns-missing
    entries: 31actionable: 0quick wins: 0linked PRs: 0
  • tag: proof
    entries: 17actionable: 0quick wins: 0linked PRs: 0
  • tag: infrastructure
    entries: 12actionable: 0quick wins: 0linked PRs: 0
  • tag: tau-ceti
    entries: 12actionable: 0quick wins: 0linked PRs: 0
  • tag: upstream
    entries: 12actionable: 0quick wins: 0linked PRs: 0
  • Show all 16 more tags
    • tag: compiled
      entries: 9actionable: 0quick wins: 0linked PRs: 0
    • tag: prime-argument
      entries: 8actionable: 0quick wins: 0linked PRs: 0
    • tag: statement-only
      entries: 7actionable: 0quick wins: 0linked PRs: 0
    • tag: integration
      entries: 6actionable: 0quick wins: 0linked PRs: 0
    • tag: planned
      entries: 5actionable: 0quick wins: 0linked PRs: 0
    • tag: modular-curves
      entries: 4actionable: 0quick wins: 0linked PRs: 0
    • tag: open
      entries: 4actionable: 0quick wins: 0linked PRs: 0
    • tag: research-open
      entries: 4actionable: 0quick wins: 0linked PRs: 0
    • tag: group-schemes
      entries: 3actionable: 0quick wins: 0linked PRs: 0
    • tag: neron
      entries: 3actionable: 0quick wins: 0linked PRs: 0
    • tag: eisenstein
      entries: 2actionable: 0quick wins: 0linked PRs: 0
    • tag: audit
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: hecke
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: mathlib
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: number-theory
      entries: 1actionable: 0quick wins: 0linked PRs: 0
    • tag: release
      entries: 1actionable: 0quick wins: 0linked PRs: 0
Metadata audit
Missing owner48
Missing owner (48)
  • «MT-API-INTEGRATION»(Theorem)
    Missing owner metadata.
    effort: mediumpriority: hightag: integrationtag: blockedtag: statement-onlytag: mazur
  • «MT-BASE-INTEGRATED»(Theorem)
    Missing owner metadata.
    effort: largepriority: hightag: milestonetag: donetag: integratedtag: mazur
  • «MT-CYCLOTOMIC-UNRAMIFIED»(Theorem)
    Missing owner metadata.
    effort: largepriority: hightag: prooftag: plannedtag: statement-onlytag: number-theory
  • «MT-EC-ISOGENY-WEIL»(Definition)
    Missing owner metadata.
    effort: largepriority: hightag: infrastructuretag: plannedtag: nouns-missingtag: mathlib
  • «MT-EXPOSITION-AUDIT»(Theorem)
    Missing owner metadata.
    effort: mediumpriority: hightag: integrationtag: blockedtag: statement-onlytag: audit
  • «MT-FFGS-BASIC»(Definition)
    Missing owner metadata.
    effort: largepriority: hightag: infrastructuretag: plannedtag: nouns-missingtag: group-schemes
  • «MT-FFGS-CONNECTED-ETALE»(Theorem)
    Missing owner metadata.
    effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: group-schemes
  • «MT-FFGS-OORT-RAYNAUD»(Theorem)
    Missing owner metadata.
    effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: group-schemes
  • «MT-FINAL-ASSEMBLY»(Theorem)
    Missing owner metadata.
    effort: mediumpriority: hightag: integrationtag: blockedtag: compiledtag: mazur
  • «MT-FINITE-JOIN»(Theorem)
    Missing owner metadata.
    effort: mediumpriority: hightag: integrationtag: blockedtag: statement-onlytag: mazur
  • Show all 38 more entries missing owner
    • «MT-NERON-BASE»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: neron
    • «MT-NERON-COMPONENTS»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: neron
    • «MT-NERON-SPECIALIZATION»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: neron
    • «MT-O25-EXCLUDE»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: research-opentag: compiledtag: mazur
    • «MT-O35-EXCLUDE»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: research-opentag: compiledtag: mazur
    • «MT-O49-TOWER»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: opentag: compiledtag: mazur
    • «MT-PIN-MIGRATION»(Theorem)
      Missing owner metadata.
      effort: mediumpriority: hightag: integrationtag: plannedtag: statement-onlytag: release
    • «MT-PRIME-DIVISION-FIELD»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: prime-argument
    • «MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: prime-argument
    • «MT-PRIME-HERBRAND-KUMMER»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: prime-argument
    • «MT-PRIME-ISOGENY-CHAIN»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: prime-argument
    • «MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: prime-argument
    • «MT-PRIME-SEMISTABLE»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: prime-argument
    • «MT-PRIME-SHAFAREVICH»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: prime-argument
    • «MT-PRIME-SPLIT-SEQUENCE»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: prime-argument
    • «MT-TC-A1-ORDER-SUPPORT»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: opentag: compiledtag: tau-ceti
    • «MT-TC-A2-PRODUCT-FORMULA»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: statement-onlytag: tau-ceti
    • «MT-TC-A3-DIVISOR-LINE-BUNDLE»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-TC-B1-COHERENT-COHOMOLOGY»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-TC-B2-RR-SERRE»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-TC-C1-RELATIVE-COHOMOLOGY»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-TC-C2-SYMMETRIC-POWERS»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-TC-D1-PICARD-FUNCTOR»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-TC-E0-PRODUCT-DIM»(Theorem)
      Missing owner metadata.
      effort: mediumpriority: hightag: upstreamtag: opentag: compiledtag: tau-ceti
    • «MT-TC-E1-JACOBIAN-VARIETY»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-TC-F1-ABEL-JACOBI»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: upstreamtag: blockedtag: nouns-missingtag: tau-ceti
    • «MT-X0-CUSPS»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: modular-curves
    • «MT-X0-EISENSTEIN-ALGEBRA»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: eisenstein
    • «MT-X0-EISENSTEIN-QUOTIENT»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: blockedtag: nouns-missingtag: eisenstein
    • «MT-X0-HECKE»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: hecke
    • «MT-X0-INTEGRAL»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: modular-curves
    • «MT-X0-JACOBIAN»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: infrastructuretag: blockedtag: nouns-missingtag: modular-curves
    • «MT-X0-MODULI»(Definition)
      Missing owner metadata.
      effort: largepriority: hightag: infrastructuretag: plannedtag: nouns-missingtag: modular-curves
    • «MT-X11-COSET»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: opentag: compiledtag: mazur
    • «MT-X11-JOIN»(Theorem)
      Missing owner metadata.
      effort: smallpriority: hightag: integrationtag: blockedtag: statement-onlytag: mazur
    • «MT-X13-NONCUSP»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: research-opentag: compiledtag: mazur
    • «MT-X18-NONCUSP»(Theorem)
      Missing owner metadata.
      effort: largepriority: hightag: prooftag: research-opentag: compiledtag: mazur
Structure and coverage
Informal-only48Statements with no associated Lean code yet.
Ready to formalize1Entries with an actionable next formalization step.
Blocked or incomplete47Entries not covered by the highlighted readiness buckets above.
Heaviest prerequisites (47)
  • «MT-FINITE-JOIN»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 3
  • «MT-X0-EISENSTEIN-QUOTIENT»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 8
  • «MT-API-INTEGRATION»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
  • «MT-TC-D2-PICARD-REPRESENTABILITY»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 20
  • «MT-X0-JACOBIAN»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 11
  • «MT-NERON-BASE»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 13
  • «MT-PRIME-DIVISION-FIELD»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 6
  • «MT-PRIME-EISENSTEIN-SPECIALIZATION»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 7
  • «MT-PRIME-ISOGENY-CHAIN»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
  • «MT-PRIME-SEMISTABLE»(Theorem)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 9
  • Show all 37 more heaviest-prerequisite entries
    • «MT-PRIME-SHAFAREVICH»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
    • «MT-PRIME-SPLIT-SEQUENCE»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 4
    • «MT-TC-C2-SYMMETRIC-POWERS»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 21
    • «MT-TC-D1-PICARD-FUNCTOR»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 21
    • «MT-TC-E1-JACOBIAN-VARIETY»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 19
    • «MT-TC-F1-ABEL-JACOBI»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 12
    • «MT-X0-HECKE»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 10
    • «MT-CYCLOTOMIC-UNRAMIFIED»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 7
    • «MT-EC-ISOGENY-WEIL»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 17
    • «MT-EXPOSITION-AUDIT»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «MT-FFGS-BASIC»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 13
    • «MT-FFGS-CONNECTED-ETALE»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 12
    • «MT-FFGS-OORT-RAYNAUD»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 11
    • «MT-FINAL-ASSEMBLY»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
    • «MT-NERON-COMPONENTS»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 12
    • «MT-NERON-SPECIALIZATION»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 11
    • «MT-O25-EXCLUDE»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
    • «MT-O35-EXCLUDE»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
    • «MT-O49-TOWER»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
    • «MT-PIN-MIGRATION»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
    • «MT-PRIME-HERBRAND-KUMMER»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
    • «MT-PRIME-OUTSIDE-IDENTITY»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 8
    • «MT-TC-A1-ORDER-SUPPORT»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 28
    • «MT-TC-A2-PRODUCT-FORMULA»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 27
    • «MT-TC-A3-DIVISOR-LINE-BUNDLE»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 26
    • «MT-TC-B1-COHERENT-COHOMOLOGY»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 25
    • «MT-TC-B2-RR-SERRE»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 21
    • «MT-TC-C1-RELATIVE-COHOMOLOGY»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 23
    • «MT-TC-E0-PRODUCT-DIM»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 20
    • «MT-X0-CUSPS»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
    • «MT-X0-EISENSTEIN-ALGEBRA»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
    • «MT-X0-INTEGRAL»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 13
    • «MT-X0-MODULI»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 14
    • «MT-X11-COSET»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 5
    • «MT-X11-JOIN»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
    • «MT-X13-NONCUSP»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
    • «MT-X18-NONCUSP»(Theorem)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 4
No prerequisites (1)
No dependents (1)