LeanBridge Blueprint

Blueprint Summary🔗

Overview
Total entries391completed: 0; deps incomplete: 0; sorries: 0; no proof: 0
Ready now0Entries whose next formalization step is currently unblocked.
Fully closed0Local code and prerequisite closure are both complete.
Actionable priorities31Entries ready now and already unlocking downstream work.
Ready next (31)
  • «alg.binary_operation»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 9downstream unlocks: 284
  • «nf.degree»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 15downstream unlocks: 188
  • «ag.riemann_surface»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 117
  • «ag.singular_point»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 115
  • «character.dirichlet»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 29downstream unlocks: 85
  • «nf.is_galois»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 6downstream unlocks: 85
  • «group.sl2z»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 9downstream unlocks: 80
  • «character.dirichlet.modulus»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 10downstream unlocks: 67
  • «nf.absolute_value»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 4downstream unlocks: 34
  • «nf.real_embedding»(Definition)
    Ready for statement work.
    stage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 31
  • Show all 21 more priorities
    • «lfunction.euler_product»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 31
    • «specialfunction.gamma»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 30
    • «lfunction.dirichlet_series»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 27
    • «ec.q.minimal_weierstrass_equation»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 7downstream unlocks: 21
    • «nf.ramified_primes»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 21
    • «gg.galois_group»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 19
    • «gl2.profinite»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 12
    • «group.maximal_subgroup»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 11
    • «gl2.cartan»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 8
    • «g2c.discriminant»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 8
    • «lfunction.self-dual»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 6
    • «ec.scheme»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 4
    • «gl2.borel»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 3downstream unlocks: 3
    • «cmf.congruence_subgroup»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 3
    • «alg.symplectic_isomorphism»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 3
    • «st_group.symplectic_form»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 3
    • af(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2
    • «af.multiplicative»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2
    • «modcurve.cusps»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 2
    • «af.bernoulli_numbers»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
    • «mf.half_integral_weight.dedekind_eta»(Definition)
      Ready for statement work.
      stage: statementstatement: ready to formalizedirect uses: 1downstream unlocks: 1
Entry index (391)
Definitions391completed: 0; deps incomplete: 0; sorries: 0; no proof: 0
Informal-only entries391
Definition Index (391)
Dependency insights
Statement-used entries291Entries reused in statement dependencies.
Most used in statements (291)
  • nf(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 92proof uses: 0direct uses: 92downstream unlocks: 170
  • ec(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 83proof uses: 0direct uses: 83downstream unlocks: 113
  • «cmf.newform»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 36proof uses: 0direct uses: 36downstream unlocks: 50
  • «character.dirichlet»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 29proof uses: 0direct uses: 29downstream unlocks: 85
  • «cmf.weight»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 28proof uses: 0direct uses: 28downstream unlocks: 67
  • «cmf.level»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 21proof uses: 0direct uses: 21downstream unlocks: 64
  • «ag.abelian_variety»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 20proof uses: 0direct uses: 20downstream unlocks: 76
  • group(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 16proof uses: 0direct uses: 16downstream unlocks: 279
  • «ring.field»(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 16proof uses: 0direct uses: 16downstream unlocks: 184
  • cmf(Definition)
    Reverse dependencies recorded in statement dependencies.
    statement uses: 16proof uses: 0direct uses: 16downstream unlocks: 72
  • Show all 281 more statement-used entries
    • «nf.degree»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 15proof uses: 0direct uses: 15downstream unlocks: 188
    • «cmf.cusp_form»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 15proof uses: 0direct uses: 15downstream unlocks: 64
    • «nf.ring_of_integers»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 14proof uses: 0direct uses: 14downstream unlocks: 92
    • «ec.weierstrass_coeffs»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 56
    • «cmf.galois_orbit»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 27
    • «cmf.coefficient_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 13proof uses: 0direct uses: 13downstream unlocks: 24
    • ring(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 12proof uses: 0direct uses: 12downstream unlocks: 217
    • lfunction(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 12proof uses: 0direct uses: 12downstream unlocks: 26
    • «cmf.character»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 11proof uses: 0direct uses: 11downstream unlocks: 57
    • «character.dirichlet.modulus»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 67
    • «cmf.hecke_operator»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 56
    • «nf.discriminant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 28
    • «ec.mordell_weil_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 16
    • «alg.binary_operation»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 284
    • «ag.variety»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 122
    • «group.sl2z»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 80
    • «ec.discriminant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 51
    • «ec.j_invariant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 27
    • «character.dirichlet.galois_orbit»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 14
    • «nf.prime»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 52
    • «ec.isogeny»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 42
    • «nf.cm_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 24
    • «ec.isogeny_class»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 8proof uses: 0direct uses: 8downstream unlocks: 17
    • «group.subgroup»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 210
    • «cmf.fouriercoefficients»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 65
    • «cmf.newspace»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 52
    • «lfunction.functional_equation»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 29
    • artin(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 25
    • «ec.q.minimal_weierstrass_equation»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 21
    • «character.dirichlet.primitive»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 19
    • «cmf.q-expansion»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 17
    • «gl2.open»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 11
    • «ec.galois_rep»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 7
    • «ec.q.conductor»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 7
    • «nf.is_galois»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 85
    • «character.dirichlet.induce»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 66
    • «ag.endomorphism_ring»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 51
    • «ring.integral_domain»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 37
    • «nf.class_number»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 29
    • «ec.good_reduction»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 24
    • «ec.bad_reduction»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 13
    • «ec.torsion_subgroup»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 11
    • «ec.complex_multiplication»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 6proof uses: 0direct uses: 6downstream unlocks: 10
    • «ring.ideal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 153
    • «ag.curve»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 116
    • «ag.curve.smooth»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 114
    • «group.fuchsian.cusps»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 74
    • «group.galois.absolute»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 41
    • «ring.characteristic»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 40
    • «nf.galois_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 38
    • «character.dirichlet.order»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 22
    • «character.dirichlet.conductor»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 21
    • «cmf.galois_representation»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 17
    • «nf.order»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 15
    • «ec.base_change»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 12
    • «cmf.self_twist»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 11
    • «lfunction.central_point»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 11
    • «ec.minimal_discriminant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 10
    • «ec.rank»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 8
    • «ec.reduction_type»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 8
    • «cmf.embedding»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 7
    • «cmf.inner_twist»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 7
    • «alg.binary_operation.identity»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 281
    • «group.abelian»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 219
    • «ring.prime_ideal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 146
    • «ag.curve.genus»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 116
    • «cmf.petersson_scalar_product»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 62
    • «ec.endomorphism»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 47
    • «nf.separable»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 46
    • «ec.endomorphism_ring»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 45
    • «nf.galois_closure»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 42
    • «ring.field_of_fractions»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 36
    • «nf.absolute_value»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 34
    • «ec.isomorphism»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 33
    • «nf.complex_embedding»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 31
    • «group.order»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 30
    • «nf.ideal_class_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 30
    • «nf.embedding»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 26
    • «nf.totally_real»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 25
    • «ec.local_minimal_model»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 19
    • «ec.global_minimal_model»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 15
    • «ec.geom_endomorphism_ring»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 12
    • «ec.mordell_weil_theorem»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 12
    • «gl2.level»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 9
    • «character.dirichlet.galois_orbit_label»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
    • «ec.regulator»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
    • «ec.tamagawa_number»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
    • «nf.sibling»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 6
    • «cmf.dimension»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 5
    • «alg.binary_operation.inverse»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 280
    • «ring.integral»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 97
    • «mf.upper_half_plane»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 76
    • «nf.minimal_polynomial»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 33
    • «ring.fractional_ideal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 33
    • «ag.dimension»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 32
    • «nf.real_embedding»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 31
    • «cmf.newform_subspace»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 29
    • «nf.signature»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 29
    • «cmf.galois_conjugate»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 28
    • «lf.local_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 26
    • «lf.ring_of_integers»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 24
    • «character.dirichlet.principal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 23
    • «nf.integral»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 22
    • «ec.additive_reduction»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 20
    • «character.dirichlet.value_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 16
    • «ec.q.discriminant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 15
    • «ec.q.period_lattice»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
    • «gl2.cartan»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 8
    • «cmf.relative_dimension»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 5
    • «ec.semistable»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 4
    • «cmf.twist»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
    • «gl2.borel»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 3
    • «alg.binary_operation.associative»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 280
    • «alg.binary_operation.commutative»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 220
    • «group.coset»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 78
    • «group.subgroup.index»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 64
    • «group.homomorphism»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 49
    • «ag.base_change»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 46
    • «av.isogeny»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 45
    • «lfunction.euler_product»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 31
    • «nf.totally_imaginary»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 26
    • «ring.maximal_ideal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 25
    • «ring.unit»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 25
    • «lf.maximal_ideal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 22
    • «artin.number_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
    • «ec.nonsplit_multiplicative_reduction»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
    • «ec.split_multiplicative_reduction»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
    • «lf.padic_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 21
    • «lf.inertia_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 20
    • «ag.mordell_weil»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 17
    • «group.automorphism»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 13
    • «group.subgroup.normal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 13
    • «gl2.profinite»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 12
    • «ec.multiplicative_reduction»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 10
    • «cmf.cm_form»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
    • «ec.q.real_period»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
    • «nf.weil_height»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 9
    • «ag.hyperelliptic_curve»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
    • «ec.canonical_height»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
    • «g2c.discriminant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 8
    • «lfunction.analytic_rank»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
    • «nf.place»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 6
    • «cmf.selfdual»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
    • «ec.period»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
    • «g2c.aut_grp»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
    • «nf.unit_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 5
    • «cmf.eisenstein_series»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
    • «ec.analytic_sha_order»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 4
    • «cmf.congruence_subgroup»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
    • «gl2.nonsplit_cartan»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
    • «gl2.split_cartan»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
    • «nf.fundamental_units»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
    • «character.dirichlet.minimal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «cmf.artin_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «cmf.fricke»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «cmf.label»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «ec.conductor»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «ec.q.modular_parametrization»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «ec.q.optimal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «gl2.normalizer_nonsplit_cartan»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «gl2.normalizer_split_cartan»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «lfunction.leading_coeff»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «lfunction.normalization»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «nf.abelian»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «nf.root_discriminant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 2
    • «ag.affine_space»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 123
    • «ag.projective_space»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 123
    • «ag.riemann_surface»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 117
    • «ag.singular_point»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 115
    • «group.fuchsian.cusps.width»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 66
    • «group.fuchsian.fundamental_domain»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 63
    • «ag.minimal_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 44
    • «ag.base_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 43
    • «lf.automorphism_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 39
    • «ring.zero_divisor»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 38
    • «ag.irreducible»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 33
    • «ring.principal_fractional_ideal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 31
    • «lfunction.gamma_factor»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 30
    • «specialfunction.gamma»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 30
    • «nf.integral_basis»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 29
    • «lfunction.dirichlet_series»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 27
    • «lf.residue_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 21
    • «nf.ramified_primes»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 21
    • «artin.ramified_primes»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
    • «group.sylow_subgroup»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 20
    • «artin.unramified_primes»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
    • «gg.galois_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
    • «lf.wild_inertia_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 19
    • «artin.conductor»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 18
    • «artin.parity»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 18
    • «ec.integral_model»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 16
    • «group.isomorphism»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
    • «ag.geom_endomorphism_ring»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
    • «ag.simple»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 13
    • «ag.endomorphism_algebra»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
    • «ag.geom_simple»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
    • «cmf.projective_image»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
    • «lfunction.critical_line»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
    • «ag.complex_multiplication»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
    • «ec.local_minimal_discriminant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
    • «group.characteristic_subgroup»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
    • «group.maximal_subgroup»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
    • «group.normal_series»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
    • «ec.weierstrass_isomorphism»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
    • «group.frattini_subgroup»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
    • «group.generators»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
    • «group.presentation»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 10
    • «ag.jacobian»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
    • «av.tate_module»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
    • «group.rank»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
    • «cmf.rm_form»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
    • «ec.padic_tate_module»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
    • «g2c.good_reduction»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
    • «gl2.index»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
    • «character.dirichlet.galois_orbit_index»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
    • «g2c.minimal_equation»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 7
    • «g2c.g2curve»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
    • «lfunction.self-dual»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 6
    • «group.torsion»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 5
    • «ec.scheme»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
    • «alg.symplectic_isomorphism»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «cmf.analytic_rank»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «cmf.atkin-lehner»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «cmf.eisenstein_form»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «ec.q»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «ec.ring»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «lfunction.arithmetic»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «ring.a-field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • «st_group.symplectic_form»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
    • af(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «af.multiplicative»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «ag.quotient_curve»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «av.twist»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «cmf.bad_prime»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «cmf.eisenstein_newspace»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «ec.torsion_order»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «gl2.normalizer_cartan»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «group.haar_measure»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «modcurve.cusps»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «modcurve.level_structure»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «modcurve.xn»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «nf.poly_discriminant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «nf.separable_algebra»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «nf.totally_positive»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «ring.integrally_closed»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «ring.noetherian»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • «st_group.usp»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
    • modcurve(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «af.bernoulli_numbers»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «af.divisor_function»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «av.simple»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «cmf.coefficient_ring»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «cmf.eisenstein_newform»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «cmf.inner_twist_count»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «cmf.satake_parameters»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «cmf.space»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «cmf.twist_minimal»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ec.bsdconjecture»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ec.kodaira_symbol»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ec.potential_good_reduction»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ec.q.bsdconjecture»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ec.q.faltings_height»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ec.q.j_invariant»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ec.q.reduction_type»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ec.twists»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «gl2.exceptional»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «lfunction.dual»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «lfunction.rh»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «lfunction.sign»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «mf.half_integral_weight.dedekind_eta»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «nf.conductor»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «nf.defining_polynomial»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «nf.local_algebra»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «nf.narrow_class_group»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «nf.polredabs»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «nf.reflex_field»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «nf.regulator»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «nf.zk_index»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ring.dedekind_domain»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «ring.irreducible»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
    • «st_group.definition»(Definition)
      Reverse dependencies recorded in statement dependencies.
      statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
Metadata
Metadata audit
Missing owner391
Missing effort391
Untagged391
Missing owner (391)
Missing effort (391)
Untagged (391)
Structure and coverage
Informal-only391Statements with no associated Lean code yet.
Heaviest prerequisites (352)
  • «ec.analytic_sha_order»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 16statement deps: 16proof deps: 0direct uses: 2downstream unlocks: 4
  • «ec.bsdconjecture»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 15statement deps: 15proof deps: 0direct uses: 1downstream unlocks: 1
  • modcurve(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 11statement deps: 11proof deps: 0direct uses: 1downstream unlocks: 1
  • «cmf.subspaces»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 11statement deps: 11proof deps: 0direct uses: 0downstream unlocks: 0
  • «ec.q.bsdconjecture»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 11statement deps: 11proof deps: 0direct uses: 1downstream unlocks: 1
  • «cmf.eisenstein_label»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 10statement deps: 10proof deps: 0direct uses: 0downstream unlocks: 0
  • «cmf.inner_twist»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 10statement deps: 10proof deps: 0direct uses: 5downstream unlocks: 7
  • «cmf.label»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 10statement deps: 10proof deps: 0direct uses: 2downstream unlocks: 2
  • «ec.invariants»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 10statement deps: 10proof deps: 0direct uses: 0downstream unlocks: 0
  • «ec.period»(Definition)
    Prerequisite fan-in measured from the current statement/proof dependency graph.
    total deps: 10statement deps: 10proof deps: 0direct uses: 2downstream unlocks: 5
  • Show all 342 more heaviest-prerequisite entries
    • «ring.dedekind_domain»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 10statement deps: 10proof deps: 0direct uses: 1downstream unlocks: 1
    • «cmf.eisenstein_newspace»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 9statement deps: 9proof deps: 0direct uses: 1downstream unlocks: 2
    • «cmf.labels»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.newspace»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 9statement deps: 9proof deps: 0direct uses: 7downstream unlocks: 52
    • «cmf.oldspace»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.galois_rep_modell_image»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.padic_completion»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 9statement deps: 9proof deps: 0direct uses: 0downstream unlocks: 0
    • «ag.complex_multiplication»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 11
    • «artin.conductor»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 18
    • «cmf.embedding»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 5downstream unlocks: 7
    • «cmf.self_twist»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 5downstream unlocks: 11
    • «cmf.twist»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 3downstream unlocks: 3
    • «ec.complex_multiplication»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 6downstream unlocks: 10
    • «ec.galois_rep»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 7downstream unlocks: 7
    • «ec.isogeny»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 8downstream unlocks: 42
    • «ec.maximal_galois_rep»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.minimal_discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 5downstream unlocks: 10
    • «ec.q.minimal_twist»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 0downstream unlocks: 0
    • «st_group.definition»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 8statement deps: 8proof deps: 0direct uses: 1downstream unlocks: 1
    • «cmf.dualform»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.eisenstein_form»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 3
    • «cmf.eisenstein»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.inner_twist_count»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 1
    • «cmf.minimal_twist»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.q-expansion»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 7downstream unlocks: 17
    • «cmf.selfdual»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 2downstream unlocks: 5
    • «cmf.twist_minimal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 1downstream unlocks: 1
    • «ec.bad_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 6downstream unlocks: 13
    • «ec.conductor»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 2downstream unlocks: 2
    • «ec.global_minimal_model»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 4downstream unlocks: 15
    • «ec.q.analytic_rank»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.rank»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 5downstream unlocks: 8
    • «ec.reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.regulator»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 7statement deps: 7proof deps: 0direct uses: 4downstream unlocks: 6
    • «character.dirichlet.galois_orbit_index»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 7
    • «character.dirichlet.minimal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 2downstream unlocks: 2
    • «cmf.cusp_form»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 15downstream unlocks: 64
    • «cmf.hecke_operator»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 10downstream unlocks: 56
    • «cmf.satake_parameters»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 1
    • «cmf.trace_bound»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.twist_multiplicity»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.mw_generators»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.cremona_label»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.lmfdb_label»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.manin_constant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.period_lattice»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 3downstream unlocks: 8
    • «ec.semi_global_minimal_model»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.simple_equation»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.special_value»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.twists»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 1
    • «modcurve.level_structure»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 2
    • «modcurve.xn»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 1downstream unlocks: 2
    • «nf.arithmetically_equivalent»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.embedding»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 4downstream unlocks: 26
    • «nf.place»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 6statement deps: 6proof deps: 0direct uses: 2downstream unlocks: 6
    • ring(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 12downstream unlocks: 217
    • «character.dirichlet.galois_orbit»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 9downstream unlocks: 14
    • «cmf.analytic_rank»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 3
    • «cmf.embedding_label»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.galois_representation»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 5downstream unlocks: 17
    • «cmf.inner_twist_multiplicity»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.projective_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.space»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
    • «cmf.sturm_bound»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.local_data»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.local_minimal_model»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 4downstream unlocks: 19
    • «ec.maximal_elladic_galois_rep»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.potential_good_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
    • «ec.q.endomorphism_ring»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.faltings_height»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
    • «ec.q.faltings_ratio»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q_curve»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.reduction_type»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 5downstream unlocks: 8
    • «g2c.minimal_equation»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 7
    • «lf.maximal_ideal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 2downstream unlocks: 22
    • «nf.class_number_formula»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.galois_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 5downstream unlocks: 38
    • «nf.minimal_sibling»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.narrow_class_number»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.reflex_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 5statement deps: 5proof deps: 0direct uses: 1downstream unlocks: 1
    • cmf(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 16downstream unlocks: 72
    • group(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 16downstream unlocks: 279
    • «ag.minimal_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 44
    • «ag.variety»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 9downstream unlocks: 122
    • «character.dirichlet.primitive»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 7downstream unlocks: 19
    • «cmf.artin_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 2
    • «cmf.artin_image»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.distinguishing_primes»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.fricke»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 2
    • «cmf.maximal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.newform_subspace»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 29
    • «cmf.stark_unit»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.sturm_bound_gamma1»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.trace_form»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.canonical_height»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 8
    • «ec.discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 9downstream unlocks: 51
    • «ec.endomorphism_ring»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 45
    • «ec.galois_rep_adelic_image»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.good_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 6downstream unlocks: 24
    • «ec.j_invariant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 9downstream unlocks: 27
    • «ec.kodaira_symbol»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 1
    • «ec.mordell_weil_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 10downstream unlocks: 16
    • «ec.multiplicative_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 10
    • «ec.obstruction_class»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.regulator»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.serre_invariants»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.szpiro_ratio»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.torsion_growth»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.ring»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 3
    • «ec.torsion_order»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 2
    • «group.rank»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 1downstream unlocks: 9
    • «group.subgroup.normal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 13
    • «group.subgroup»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 7downstream unlocks: 210
    • «lf.inertia_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 2downstream unlocks: 20
    • «nf.ideal_class_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 4downstream unlocks: 30
    • «nf.relative_class_number»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.serre_odlyzko_bound»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.signature»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 4statement deps: 4proof deps: 0direct uses: 3downstream unlocks: 29
    • ec(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 83downstream unlocks: 113
    • lfunction(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 12downstream unlocks: 26
    • «ag.quotient_curve»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
    • «artin.ramified_primes»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 20
    • «artin.unramified_primes»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 19
    • «character.dirichlet.galois_orbit_label»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 6
    • «character.dirichlet.order»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 22
    • «character.dirichlet.principal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 23
    • «cmf.atkin-lehner»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 3
    • «cmf.coefficient_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 13downstream unlocks: 24
    • «cmf.dimension»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 5
    • «cmf.eisenstein_newform»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
    • «cmf.eisenstein_series»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 4
    • «cmf.fouriercoefficients»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 7downstream unlocks: 65
    • «cmf.galois_orbit»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 13downstream unlocks: 27
    • «cmf.hecke_orbit»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.hecke_ring_generators»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.heckecharpolys»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.newform»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 36downstream unlocks: 50
    • «cmf.petersson_scalar_product»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 62
    • «cmf.projective_image»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 12
    • «cmf.sato_tate»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.endomorphism»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 47
    • «ec.geom_endomorphism_ring»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 12
    • «ec.integral_model»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 16
    • «ec.isogeny_class_degree»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.local_minimal_discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 11
    • «ec.mordell_weil_theorem»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 12
    • «ec.padic_tate_module»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 8
    • «ec.q.abc_quality»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.canonical_height»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.conductor»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 7downstream unlocks: 7
    • «ec.q.discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 15
    • «ec.q.j_invariant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
    • «ec.q.optimal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
    • «ec.q.real_period»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 9
    • «ec.q.semistable»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.special_value»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.semistable»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 4
    • «ec.tamagawa_number»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 6
    • «g2c.g2curve»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 6
    • «gl2.index»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 8
    • «group.abelian»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 4downstream unlocks: 219
    • «group.characteristic_subgroup»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 11
    • «group.frattini_subgroup»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 10
    • «group.normal_series»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 11
    • «group.sylow_subgroup»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 20
    • «lf.local_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 3downstream unlocks: 26
    • «lf.wild_inertia_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 19
    • «lfunction.central_point»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 11
    • «nf.cm_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 8downstream unlocks: 24
    • «nf.dirichlet_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.galois_root_discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.generator»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.maximal_cm_subfield»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.monomial_order»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.poly_discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
    • «nf.prime»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 8downstream unlocks: 52
    • «nf.root_discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 2downstream unlocks: 2
    • «nf.zk_index»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 1
    • «ring.characteristic»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 5downstream unlocks: 40
    • «ring.integrally_closed»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 2
    • artin(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 25
    • «af.divisor_function»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «ag.abelian_variety»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 20downstream unlocks: 76
    • «ag.base_change»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 46
    • «ag.base_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 43
    • «ag.curve.smooth»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 114
    • «ag.dimension»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 32
    • «ag.endomorphism_algebra»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 12
    • «ag.geom_simple»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 12
    • «ag.hyperelliptic_curve»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 8
    • «ag.mordell_weil»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 17
    • «alg.binary_operation.inverse»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 280
    • «artin.number_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 21
    • «av.tate_module»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 9
    • «av.twist»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
    • «character.dirichlet.induce»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 66
    • «cmf.bad_prime»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
    • «cmf.character»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 11downstream unlocks: 57
    • «cmf.cm_form»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 9
    • «cmf.coefficient_ring»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «cmf.decomposition.new.gamma0chi»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.defining_polynomial»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.galois_conjugate»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 28
    • «cmf.level»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 21downstream unlocks: 64
    • «cmf.nontrivial_twist»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.rm_form»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 8
    • «cmf.space_trace_form»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.additive_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 20
    • «ec.good_ordinary_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.good_supersingular_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.isogeny_class»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 8downstream unlocks: 17
    • «ec.isogeny_graph»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.isogeny_matrix»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.isomorphism»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 33
    • «ec.nonsplit_multiplicative_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 21
    • «ec.q.analytic_sha_order»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.kodaira_symbol»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.modular_degree»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q.naive_height»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ec.q»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 3
    • «ec.split_multiplicative_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 21
    • «ec.torsion_subgroup»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 11
    • «ec.weierstrass_isomorphism»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 10
    • «g2c.aut_grp»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
    • «g2c.good_reduction»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 8
    • «gl2.exceptional»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «group.automorphism»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 13
    • «group.coset»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 78
    • «group.fuchsian.cusps.width»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 66
    • «group.generators»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 10
    • «group.haar_measure»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
    • «group.torsion»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 5
    • «lf.automorphism_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 39
    • «lf.padic_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 21
    • «lf.residue_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 21
    • «lf.ring_of_integers»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 24
    • «lfunction.analytic_rank»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 6
    • «lfunction.critical_line»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 12
    • «lfunction.functional_equation»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 29
    • «lfunction.leading_coeff»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
    • «nf.abelian»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
    • «nf.abs_discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.class_number»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 29
    • «nf.complex_embedding»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 31
    • «nf.conductor»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «nf.discriminant»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 10downstream unlocks: 28
    • «nf.fundamental_units»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 3
    • «nf.inessential_prime»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.integral_basis»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 29
    • «nf.integral»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 22
    • «nf.local_algebra»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «nf.monogenic»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.narrow_class_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «nf.polredabs»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «nf.rank»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.reflex_reflex_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.regulator»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «nf.ring_of_integers»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 14downstream unlocks: 92
    • «nf.sibling»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 6
    • «nf.stem_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.torsion»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.unit_group»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
    • «nf.unramified_prime»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.weil_height»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 9
    • «nf.weil_polynomial»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
    • «ring.field_of_fractions»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 36
    • «ring.field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 16downstream unlocks: 184
    • «ring.fractional_ideal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 33
    • «ring.ideal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 153
    • «ring.integral_domain»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 6downstream unlocks: 37
    • «ring.irreducible»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
    • «ring.maximal_ideal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 25
    • «ring.noetherian»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
    • «ring.prime_ideal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 4downstream unlocks: 146
    • «ring.principal_fractional_ideal»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 31
    • «ring.unit»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 25
    • nf(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 92downstream unlocks: 170
    • «ag.affine_space»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 123
    • «ag.curve.genus»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 116
    • «ag.curve»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 116
    • «ag.endomorphism_ring»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 6downstream unlocks: 51
    • «ag.geom_endomorphism_ring»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 13
    • «ag.irreducible»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 33
    • «ag.jacobian»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 9
    • «ag.projective_space»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 123
    • «ag.simple»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 13
    • «alg.binary_operation.associative»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 280
    • «alg.binary_operation.commutative»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 220
    • «alg.binary_operation.identity»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 281
    • «artin.parity»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 18
    • «av.isogeny»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 45
    • «av.simple»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
    • «character.dirichlet.conductor»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 21
    • «character.dirichlet.value_field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 16
    • «cmf.analytic_conductor»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.eta_quotient»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.minus_space»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.plus_space»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.relative_dimension»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 5
    • «cmf.satake_angles»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.shimura_correspondence»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «cmf.weight»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 28downstream unlocks: 67
    • «ec.base_change»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 12
    • «ec.q.modular_parametrization»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
    • «ec.q.reduction_type»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
    • «ec.weierstrass_coeffs»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 13downstream unlocks: 56
    • «gl2.level»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 9
    • «gl2.nonsplit_cartan»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
    • «gl2.normalizer_cartan»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
    • «gl2.normalizer_nonsplit_cartan»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
    • «gl2.normalizer_split_cartan»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
    • «gl2.open»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 7downstream unlocks: 11
    • «gl2.split_cartan»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
    • «group.fuchsian.cusps»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 74
    • «group.fuchsian.fundamental_domain»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 63
    • «group.galois.absolute»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 41
    • «group.homomorphism»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 49
    • «group.isomorphism»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 14
    • «group.order»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 30
    • «group.presentation»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 10
    • «group.subgroup.index»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 64
    • «lfunction.arithmetic»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
    • «lfunction.dual»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
    • «lfunction.gamma_factor»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 30
    • «lfunction.normalization»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 2
    • «lfunction.rh»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
    • «lfunction.sign»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
    • «mf.upper_half_plane»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 76
    • «nf.defining_polynomial»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
    • «nf.galois_closure»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 42
    • «nf.ideal_labels»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
    • «nf.minimal_polynomial»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 33
    • «nf.order»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 15
    • «nf.separable_algebra»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
    • «nf.separable»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 46
    • «nf.totally_imaginary»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 26
    • «nf.totally_positive»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
    • «nf.totally_real»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 25
    • «ring.a-field»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
    • «ring.integral»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 97
    • «ring.zero_divisor»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 38
    • «st_group.usp»(Definition)
      Prerequisite fan-in measured from the current statement/proof dependency graph.
      total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
No prerequisites (39)
No dependents (100)