Blueprint Summary🔗

Overview

Total entries52completed: 19; deps incomplete: 28; sorries: 0; no proof: 1

Ready now1Entries whose next formalization step is currently unblocked.

Fully closed19Local code and prerequisite closure are both complete.

Actionable priorities3Entries ready now and already unlocking downstream work.

Current blockers1Missing external or incomplete Lean declarations.

Missing informal coverage4Entries with Lean code but missing an informal statement or proof block.

Ready next (3)

«def:decomposition-group»(Definition)

Ready for statement work.

stage: statementstatement: ready to formalizedirect uses: 2downstream unlocks: 28
«lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 2downstream unlocks: 12proof: ready to formalize
Associated lean decls (1)
- Chebotarev.tendsto_ratio_one_of_log_pm_bounded
«lem:H-n-over-H-formula»(Lemma)

Ready for proof work.

stage: proofstatement: ready to formalizedirect uses: 1downstream unlocks: 8proof: ready to formalize

Current blockers (1)

«lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)

Missing external Lean declaration: Chebotarev.tendsto_ratio_one_of_log_pm_bounded [missing declaration]

Missing informal coverage (4)

«lem:exists-frobenius-class»(Lemma)
Associated lean decls (1)
- Chebotarev.exists_frobeniusClass
«thm:chebotarev-cyclotomic»(Theorem)
Associated lean decls (1)
- Chebotarev.chebotarev_cyclotomic
«lem:prime-zeta-higher-tail-bounded»(Lemma)
Associated lean decls (1)
- Chebotarev.primeIdealZetaHigherTail_bounded
«lem:character-orthogonality-eq»(Lemma)
Associated lean decls (1)
- Chebotarev.character_orthogonality_cyclotomic_eq

Entry index (52)

Definitions7completed: 3; deps incomplete: 1; sorries: 0; no proof: 0

Lemmas37completed: 16; deps incomplete: 19; sorries: 0; no proof: 1

Theorems5completed: 0; deps incomplete: 5; sorries: 0; no proof: 0

Corollaries3completed: 0; deps incomplete: 3; sorries: 0; no proof: 0

Informal-only entries4

Definition Index (7)

«def:frobenius-class»(Definition)
Associated lean decls (1)
- Chebotarev.frobeniusClass
«def:unramified-in»(Definition)
Associated lean decls (1)
- Chebotarev.UnramifiedIn
«def:frobenius-at»(Definition)
«def:decomposition-group»(Definition)
«def:dirichlet-density»(Definition)
Associated lean decls (1)
- Chebotarev.HasDirichletDensity
«def:galois-character»(Definition)
Associated lean decls (1)
- Chebotarev.galoisCharacter
«def:inertia-group»(Definition)

Theorem / Proposition / Lemma / Corollary Index (45)

«lem:logzeta-eq-primesum-bounded»(Lemma)
Associated lean decls (1)
- Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded
«lem:H-n-over-H-tends-one»(Lemma)
Associated lean decls (1)
- Chebotarev.H_n_over_H_tends_to_one
«lem:ratiosum-fibres-tendsto-one»(Lemma)
Associated lean decls (1)
- Chebotarev.ratioSum_frobeniusFibres_tendsto_one
«lem:conjclasses-carrier-card-pos»(Lemma)
Associated lean decls (1)
- Chebotarev.ConjClasses_carrier_card_pos
«lem:H-n-over-H-formula»(Lemma)
«cor:dirichlet-ap-density»(Corollary)
Associated lean decls (1)
- Chebotarev.dirichlet_primes_in_AP
«lem:log-artin-asymp-character-sum»(Lemma)
Associated lean decls (1)
- Chebotarev.log_artinLSeries_asymp_character_sum
«lem:prime-zeta-ge-log-minus-bounded»(Lemma)
Associated lean decls (1)
- Chebotarev.log_minus_bounded_le_primeIdealZetaSum
«lem:logzeta-eq-loginv-bounded»(Lemma)
Associated lean decls (1)
- Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded
«lem:exists-frobenius-class»(Lemma)
Associated lean decls (1)
- Chebotarev.exists_frobeniusClass
«lem:prime-zeta-le-log-plus-bounded»(Lemma)
Associated lean decls (1)
- Chebotarev.primeIdealZetaSum_le_log_plus_bounded
«lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)
Associated lean decls (1)
- Chebotarev.tendsto_ratio_one_of_log_pm_bounded
«thm:dedekind-zeta-factorisation»(Theorem)
Associated lean decls (1)
- Chebotarev.dedekindZeta_eq_prod_artinDirichletSeries
«thm:chebotarev-cyclotomic»(Theorem)
Associated lean decls (1)
- Chebotarev.chebotarev_cyclotomic
«lem:cyclic-subgroup-trivial-meet»(Lemma)
Associated lean decls (1)
- Chebotarev.cyclic_subgroup_meets_G_times_one_trivially
«lem:prime-zeta-higher-tail-bounded»(Lemma)
Associated lean decls (1)
- Chebotarev.primeIdealZetaHigherTail_bounded
«lem:conjclasses-carrier-card-one-comm»(Lemma)
Associated lean decls (1)
- Chebotarev.ConjClasses_carrier_card_eq_one_of_comm
«thm:chebotarev-density-comm»(Theorem)
Associated lean decls (1)
- Chebotarev.chebotarev_density_of_comm
«lem:character-orthogonality-eq»(Lemma)
Associated lean decls (1)
- Chebotarev.character_orthogonality_cyclotomic_eq
«lem:density-S-sigma-tau»(Lemma)
Associated lean decls (1)
- Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH
«lem:character-sum-geom-numbers»(Lemma)
Associated lean decls (1)
- Chebotarev.character_sum_geometry_of_numbers_bound
«lem:dedekind-local-factor»(Lemma)
Associated lean decls (1)
- Chebotarev.dedekindZeta_local_factor_eq_product_artin_local
«lem:artin-one-ne-zero»(Lemma)
Associated lean decls (1)
- Chebotarev.artinLSeries_one_ne_zero
«lem:density-implies-lower»(Lemma)
Associated lean decls (1)
- Chebotarev.HasDirichletDensity.hasLower
«thm:chebotarev-density»(Theorem)
Associated lean decls (1)
- Chebotarev.chebotarev_density
«lem:frobenius-class-eq-mk»(Lemma)
Associated lean decls (1)
- Chebotarev.frobeniusClass_eq_mk_of_isArithFrobAt
«lem:character-orthogonality-ne»(Lemma)
Associated lean decls (1)
- Chebotarev.character_orthogonality_cyclotomic_ne
«lem:conjclasses-mk-one-carrier-card-one»(Lemma)
Associated lean decls (1)
- Chebotarev.ConjClasses_mk_one_carrier_card_eq_one
«lem:artin-euler-product-abelian»(Lemma)
Associated lean decls (1)
- Chebotarev.exists_artinLSeries_eulerProduct_abelian
«lem:cyclotomic-density-two-sided»(Lemma)
Associated lean decls (1)
- Chebotarev.cyclotomic_density_from_two_sided_asymp
«lem:has-density-finite»(Lemma)
Associated lean decls (1)
- Chebotarev.hasDirichletDensity_of_finite
«lem:artin-analytic-extension»(Lemma)
Associated lean decls (1)
- Chebotarev.artinLSeries_analytic_extension
«lem:ratio-glue-numerator»(Lemma)
Associated lean decls (1)
- Chebotarev.tendsto_ratio_of_log_asymp_numerator
«lem:liminf-ratio-ge-inv-card-G»(Lemma)
Associated lean decls (1)
- Chebotarev.liminf_ratio_ge_inv_card_G
«thm:chebotarev-abelian»(Theorem)
Associated lean decls (1)
- Chebotarev.chebotarev_abelian
«lem:prime-ideal-sum-log»(Lemma)
Associated lean decls (1)
- Chebotarev.primeIdealZetaSum_univ_tendsto_log
«lem:density-lift-fixedfield»(Lemma)
Associated lean decls (1)
- Chebotarev.density_lift_through_fixedField
«lem:infinite-of-density-pos»(Lemma)
Associated lean decls (1)
- Chebotarev.infinite_of_hasDirichletDensity_pos
«lem:count-primes-above-frob-sigma»(Lemma)
Associated lean decls (1)
- Chebotarev.count_primes_above_with_frobenius_eq_sigma
«cor:density-split-completely»(Corollary)
Associated lean decls (1)
- Chebotarev.density_split_completely
«lem:cyclotomic-frobenius-norm-power»(Lemma)
Associated lean decls (1)
- Chebotarev.cyclotomic_frobenius_acts_as_norm_power
«lem:pigeonhole-density»(Lemma)
Associated lean decls (1)
- Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one
«lem:finite-ramified-primes»(Lemma)
Associated lean decls (1)
- Chebotarev.finite_ramifiedIn
«lem:primesum-fibre-asymp»(Lemma)
Associated lean decls (1)
- Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp
«cor:infinite-frobenius-class»(Corollary)
Associated lean decls (1)
- Chebotarev.infinite_setOf_frobenius_class

Dependency insights

Statement-used entries43Entries reused in statement dependencies.

Proof-used entries28Entries reused in proof-only dependencies.

Most used in statements (43)

«def:frobenius-class»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 10proof uses: 0direct uses: 10downstream unlocks: 23
Associated lean decls (1)
- Chebotarev.frobeniusClass
«def:frobenius-at»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 26
«def:dirichlet-density»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 12
Associated lean decls (1)
- Chebotarev.HasDirichletDensity
«def:galois-character»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 19
Associated lean decls (1)
- Chebotarev.galoisCharacter
«thm:chebotarev-density»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 3
Associated lean decls (1)
- Chebotarev.chebotarev_density
«def:decomposition-group»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 28
«def:unramified-in»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 28
Associated lean decls (1)
- Chebotarev.UnramifiedIn
«lem:artin-euler-product-abelian»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 16
Associated lean decls (1)
- Chebotarev.exists_artinLSeries_eulerProduct_abelian
«lem:logzeta-eq-loginv-bounded»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 14
Associated lean decls (1)
- Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded
«lem:logzeta-eq-primesum-bounded»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 14
Associated lean decls (1)
- Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded
Show all 33 more statement-used entries
- «lem:artin-one-ne-zero»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 13
  Associated lean decls (1)
  - Chebotarev.artinLSeries_one_ne_zero
- «lem:prime-ideal-sum-log»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_univ_tendsto_log
- «thm:chebotarev-abelian»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 2proof uses: 2direct uses: 4downstream unlocks: 5
  Associated lean decls (1)
  - Chebotarev.chebotarev_abelian
- «lem:prime-zeta-higher-tail-bounded»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 15
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaHigherTail_bounded
- «lem:character-sum-geom-numbers»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 15
  Associated lean decls (1)
  - Chebotarev.character_sum_geometry_of_numbers_bound
- «lem:artin-analytic-extension»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 14
  Associated lean decls (1)
  - Chebotarev.artinLSeries_analytic_extension
- «lem:dedekind-local-factor»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 13
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_local_factor_eq_product_artin_local
- «lem:prime-zeta-ge-log-minus-bounded»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - Chebotarev.log_minus_bounded_le_primeIdealZetaSum
- «lem:prime-zeta-le-log-plus-bounded»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_le_log_plus_bounded
- «lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_one_of_log_pm_bounded
- «thm:dedekind-zeta-factorisation»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 12
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_eq_prod_artinDirichletSeries
- «lem:character-orthogonality-eq»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_eq
- «lem:character-orthogonality-ne»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_ne
- «lem:log-artin-asymp-character-sum»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.log_artinLSeries_asymp_character_sum
- «lem:primesum-fibre-asymp»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 10
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp
- «lem:ratio-glue-numerator»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 10
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_of_log_asymp_numerator
- «lem:cyclotomic-density-two-sided»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 9
  Associated lean decls (1)
  - Chebotarev.cyclotomic_density_from_two_sided_asymp
- «lem:H-n-over-H-formula»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
- «lem:cyclic-subgroup-trivial-meet»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (1)
  - Chebotarev.cyclic_subgroup_meets_G_times_one_trivially
- «thm:chebotarev-cyclotomic»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 8
  Associated lean decls (1)
  - Chebotarev.chebotarev_cyclotomic
- «lem:H-n-over-H-tends-one»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.H_n_over_H_tends_to_one
- «lem:density-S-sigma-tau»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH
- «lem:finite-ramified-primes»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.finite_ramifiedIn
- «lem:liminf-ratio-ge-inv-card-G»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - Chebotarev.liminf_ratio_ge_inv_card_G
- «lem:pigeonhole-density»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one
- «lem:ratiosum-fibres-tendsto-one»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - Chebotarev.ratioSum_frobeniusFibres_tendsto_one
- «lem:count-primes-above-frob-sigma»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - Chebotarev.count_primes_above_with_frobenius_eq_sigma
- «lem:density-lift-fixedfield»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - Chebotarev.density_lift_through_fixedField
- «lem:conjclasses-carrier-card-one-comm»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_eq_one_of_comm
- «lem:conjclasses-carrier-card-pos»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_pos
- «lem:conjclasses-mk-one-carrier-card-one»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.ConjClasses_mk_one_carrier_card_eq_one
- «lem:exists-frobenius-class»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.exists_frobeniusClass
- «lem:infinite-of-density-pos»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.infinite_of_hasDirichletDensity_pos

Most used in proofs (28)

«lem:logzeta-eq-loginv-bounded»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 14
Associated lean decls (1)
- Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded
«lem:logzeta-eq-primesum-bounded»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 14
Associated lean decls (1)
- Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded
«lem:artin-one-ne-zero»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 13
Associated lean decls (1)
- Chebotarev.artinLSeries_one_ne_zero
«lem:prime-ideal-sum-log»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 11
Associated lean decls (1)
- Chebotarev.primeIdealZetaSum_univ_tendsto_log
«thm:chebotarev-abelian»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 2direct uses: 4downstream unlocks: 5
Associated lean decls (1)
- Chebotarev.chebotarev_abelian
«thm:chebotarev-density»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 3direct uses: 5downstream unlocks: 3
Associated lean decls (1)
- Chebotarev.chebotarev_density
«lem:prime-zeta-higher-tail-bounded»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 15
Associated lean decls (1)
- Chebotarev.primeIdealZetaHigherTail_bounded
«lem:dedekind-local-factor»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 13
Associated lean decls (1)
- Chebotarev.dedekindZeta_local_factor_eq_product_artin_local
«lem:prime-zeta-ge-log-minus-bounded»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 12
Associated lean decls (1)
- Chebotarev.log_minus_bounded_le_primeIdealZetaSum
«lem:prime-zeta-le-log-plus-bounded»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 12
Associated lean decls (1)
- Chebotarev.primeIdealZetaSum_le_log_plus_bounded
Show all 18 more proof-used entries
- «lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_one_of_log_pm_bounded
- «lem:character-orthogonality-eq»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_eq
- «lem:character-orthogonality-ne»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_ne
- «lem:primesum-fibre-asymp»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 10
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp
- «lem:ratio-glue-numerator»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 10
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_of_log_asymp_numerator
- «lem:H-n-over-H-tends-one»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.H_n_over_H_tends_to_one
- «lem:density-S-sigma-tau»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH
- «lem:finite-ramified-primes»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.finite_ramifiedIn
- «lem:liminf-ratio-ge-inv-card-G»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - Chebotarev.liminf_ratio_ge_inv_card_G
- «lem:pigeonhole-density»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one
- «lem:ratiosum-fibres-tendsto-one»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - Chebotarev.ratioSum_frobeniusFibres_tendsto_one
- «lem:count-primes-above-frob-sigma»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - Chebotarev.count_primes_above_with_frobenius_eq_sigma
- «lem:density-lift-fixedfield»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - Chebotarev.density_lift_through_fixedField
- «lem:conjclasses-carrier-card-one-comm»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_eq_one_of_comm
- «lem:conjclasses-carrier-card-pos»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_pos
- «lem:conjclasses-mk-one-carrier-card-one»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.ConjClasses_mk_one_carrier_card_eq_one
- «lem:exists-frobenius-class»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.exists_frobeniusClass
- «lem:infinite-of-density-pos»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.infinite_of_hasDirichletDensity_pos

Metadata

Metadata audit

Missing owner52

Missing effort52

Untagged52

Missing owner (52)

«cor:density-split-completely»(Corollary)

Missing owner metadata.
Associated lean decls (1)
- Chebotarev.density_split_completely
«cor:dirichlet-ap-density»(Corollary)

Missing owner metadata.
Associated lean decls (1)
- Chebotarev.dirichlet_primes_in_AP
«cor:infinite-frobenius-class»(Corollary)

Missing owner metadata.
Associated lean decls (1)
- Chebotarev.infinite_setOf_frobenius_class
«def:decomposition-group»(Definition)

Missing owner metadata.
«def:dirichlet-density»(Definition)

Missing owner metadata.
Associated lean decls (1)
- Chebotarev.HasDirichletDensity
«def:frobenius-at»(Definition)

Missing owner metadata.
«def:frobenius-class»(Definition)

Missing owner metadata.
Associated lean decls (1)
- Chebotarev.frobeniusClass
«def:galois-character»(Definition)

Missing owner metadata.
Associated lean decls (1)
- Chebotarev.galoisCharacter
«def:inertia-group»(Definition)

Missing owner metadata.
«def:unramified-in»(Definition)

Missing owner metadata.
Associated lean decls (1)
- Chebotarev.UnramifiedIn
Show all 42 more entries missing owner
- «lem:H-n-over-H-formula»(Lemma)
  
  Missing owner metadata.
- «lem:H-n-over-H-tends-one»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.H_n_over_H_tends_to_one
- «lem:artin-analytic-extension»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.artinLSeries_analytic_extension
- «lem:artin-euler-product-abelian»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.exists_artinLSeries_eulerProduct_abelian
- «lem:artin-one-ne-zero»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.artinLSeries_one_ne_zero
- «lem:character-orthogonality-eq»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_eq
- «lem:character-orthogonality-ne»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_ne
- «lem:character-sum-geom-numbers»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.character_sum_geometry_of_numbers_bound
- «lem:conjclasses-carrier-card-one-comm»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_eq_one_of_comm
- «lem:conjclasses-carrier-card-pos»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_pos
- «lem:conjclasses-mk-one-carrier-card-one»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_mk_one_carrier_card_eq_one
- «lem:count-primes-above-frob-sigma»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.count_primes_above_with_frobenius_eq_sigma
- «lem:cyclic-subgroup-trivial-meet»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.cyclic_subgroup_meets_G_times_one_trivially
- «lem:cyclotomic-density-two-sided»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.cyclotomic_density_from_two_sided_asymp
- «lem:cyclotomic-frobenius-norm-power»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.cyclotomic_frobenius_acts_as_norm_power
- «lem:dedekind-local-factor»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_local_factor_eq_product_artin_local
- «lem:density-S-sigma-tau»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH
- «lem:density-implies-lower»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.HasDirichletDensity.hasLower
- «lem:density-lift-fixedfield»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.density_lift_through_fixedField
- «lem:exists-frobenius-class»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.exists_frobeniusClass
- «lem:finite-ramified-primes»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.finite_ramifiedIn
- «lem:frobenius-class-eq-mk»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.frobeniusClass_eq_mk_of_isArithFrobAt
- «lem:has-density-finite»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.hasDirichletDensity_of_finite
- «lem:infinite-of-density-pos»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.infinite_of_hasDirichletDensity_pos
- «lem:liminf-ratio-ge-inv-card-G»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.liminf_ratio_ge_inv_card_G
- «lem:log-artin-asymp-character-sum»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.log_artinLSeries_asymp_character_sum
- «lem:logzeta-eq-loginv-bounded»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded
- «lem:logzeta-eq-primesum-bounded»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded
- «lem:pigeonhole-density»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one
- «lem:prime-ideal-sum-log»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_univ_tendsto_log
- «lem:prime-zeta-ge-log-minus-bounded»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.log_minus_bounded_le_primeIdealZetaSum
- «lem:prime-zeta-higher-tail-bounded»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaHigherTail_bounded
- «lem:prime-zeta-le-log-plus-bounded»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_le_log_plus_bounded
- «lem:primesum-fibre-asymp»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp
- «lem:ratio-glue-numerator»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_of_log_asymp_numerator
- «lem:ratiosum-fibres-tendsto-one»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.ratioSum_frobeniusFibres_tendsto_one
- «lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_one_of_log_pm_bounded
- «thm:chebotarev-abelian»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_abelian
- «thm:chebotarev-cyclotomic»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_cyclotomic
- «thm:chebotarev-density-comm»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_density_of_comm
- «thm:chebotarev-density»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_density
- «thm:dedekind-zeta-factorisation»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_eq_prod_artinDirichletSeries

Missing effort (52)

«cor:density-split-completely»(Corollary)

Missing effort metadata.
Associated lean decls (1)
- Chebotarev.density_split_completely
«cor:dirichlet-ap-density»(Corollary)

Missing effort metadata.
Associated lean decls (1)
- Chebotarev.dirichlet_primes_in_AP
«cor:infinite-frobenius-class»(Corollary)

Missing effort metadata.
Associated lean decls (1)
- Chebotarev.infinite_setOf_frobenius_class
«def:decomposition-group»(Definition)

Missing effort metadata.
«def:dirichlet-density»(Definition)

Missing effort metadata.
Associated lean decls (1)
- Chebotarev.HasDirichletDensity
«def:frobenius-at»(Definition)

Missing effort metadata.
«def:frobenius-class»(Definition)

Missing effort metadata.
Associated lean decls (1)
- Chebotarev.frobeniusClass
«def:galois-character»(Definition)

Missing effort metadata.
Associated lean decls (1)
- Chebotarev.galoisCharacter
«def:inertia-group»(Definition)

Missing effort metadata.
«def:unramified-in»(Definition)

Missing effort metadata.
Associated lean decls (1)
- Chebotarev.UnramifiedIn
Show all 42 more entries missing effort
- «lem:H-n-over-H-formula»(Lemma)
  
  Missing effort metadata.
- «lem:H-n-over-H-tends-one»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.H_n_over_H_tends_to_one
- «lem:artin-analytic-extension»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.artinLSeries_analytic_extension
- «lem:artin-euler-product-abelian»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.exists_artinLSeries_eulerProduct_abelian
- «lem:artin-one-ne-zero»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.artinLSeries_one_ne_zero
- «lem:character-orthogonality-eq»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_eq
- «lem:character-orthogonality-ne»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_ne
- «lem:character-sum-geom-numbers»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.character_sum_geometry_of_numbers_bound
- «lem:conjclasses-carrier-card-one-comm»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_eq_one_of_comm
- «lem:conjclasses-carrier-card-pos»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_pos
- «lem:conjclasses-mk-one-carrier-card-one»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_mk_one_carrier_card_eq_one
- «lem:count-primes-above-frob-sigma»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.count_primes_above_with_frobenius_eq_sigma
- «lem:cyclic-subgroup-trivial-meet»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.cyclic_subgroup_meets_G_times_one_trivially
- «lem:cyclotomic-density-two-sided»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.cyclotomic_density_from_two_sided_asymp
- «lem:cyclotomic-frobenius-norm-power»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.cyclotomic_frobenius_acts_as_norm_power
- «lem:dedekind-local-factor»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_local_factor_eq_product_artin_local
- «lem:density-S-sigma-tau»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH
- «lem:density-implies-lower»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.HasDirichletDensity.hasLower
- «lem:density-lift-fixedfield»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.density_lift_through_fixedField
- «lem:exists-frobenius-class»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.exists_frobeniusClass
- «lem:finite-ramified-primes»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.finite_ramifiedIn
- «lem:frobenius-class-eq-mk»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.frobeniusClass_eq_mk_of_isArithFrobAt
- «lem:has-density-finite»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.hasDirichletDensity_of_finite
- «lem:infinite-of-density-pos»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.infinite_of_hasDirichletDensity_pos
- «lem:liminf-ratio-ge-inv-card-G»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.liminf_ratio_ge_inv_card_G
- «lem:log-artin-asymp-character-sum»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.log_artinLSeries_asymp_character_sum
- «lem:logzeta-eq-loginv-bounded»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded
- «lem:logzeta-eq-primesum-bounded»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded
- «lem:pigeonhole-density»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one
- «lem:prime-ideal-sum-log»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_univ_tendsto_log
- «lem:prime-zeta-ge-log-minus-bounded»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.log_minus_bounded_le_primeIdealZetaSum
- «lem:prime-zeta-higher-tail-bounded»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaHigherTail_bounded
- «lem:prime-zeta-le-log-plus-bounded»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_le_log_plus_bounded
- «lem:primesum-fibre-asymp»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp
- «lem:ratio-glue-numerator»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_of_log_asymp_numerator
- «lem:ratiosum-fibres-tendsto-one»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.ratioSum_frobeniusFibres_tendsto_one
- «lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_one_of_log_pm_bounded
- «thm:chebotarev-abelian»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_abelian
- «thm:chebotarev-cyclotomic»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_cyclotomic
- «thm:chebotarev-density-comm»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_density_of_comm
- «thm:chebotarev-density»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_density
- «thm:dedekind-zeta-factorisation»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_eq_prod_artinDirichletSeries

Untagged (52)

«cor:density-split-completely»(Corollary)

Missing tag metadata.
Associated lean decls (1)
- Chebotarev.density_split_completely
«cor:dirichlet-ap-density»(Corollary)

Missing tag metadata.
Associated lean decls (1)
- Chebotarev.dirichlet_primes_in_AP
«cor:infinite-frobenius-class»(Corollary)

Missing tag metadata.
Associated lean decls (1)
- Chebotarev.infinite_setOf_frobenius_class
«def:decomposition-group»(Definition)

Missing tag metadata.
«def:dirichlet-density»(Definition)

Missing tag metadata.
Associated lean decls (1)
- Chebotarev.HasDirichletDensity
«def:frobenius-at»(Definition)

Missing tag metadata.
«def:frobenius-class»(Definition)

Missing tag metadata.
Associated lean decls (1)
- Chebotarev.frobeniusClass
«def:galois-character»(Definition)

Missing tag metadata.
Associated lean decls (1)
- Chebotarev.galoisCharacter
«def:inertia-group»(Definition)

Missing tag metadata.
«def:unramified-in»(Definition)

Missing tag metadata.
Associated lean decls (1)
- Chebotarev.UnramifiedIn
Show all 42 more untagged entries
- «lem:H-n-over-H-formula»(Lemma)
  
  Missing tag metadata.
- «lem:H-n-over-H-tends-one»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.H_n_over_H_tends_to_one
- «lem:artin-analytic-extension»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.artinLSeries_analytic_extension
- «lem:artin-euler-product-abelian»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.exists_artinLSeries_eulerProduct_abelian
- «lem:artin-one-ne-zero»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.artinLSeries_one_ne_zero
- «lem:character-orthogonality-eq»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_eq
- «lem:character-orthogonality-ne»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_ne
- «lem:character-sum-geom-numbers»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.character_sum_geometry_of_numbers_bound
- «lem:conjclasses-carrier-card-one-comm»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_eq_one_of_comm
- «lem:conjclasses-carrier-card-pos»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_pos
- «lem:conjclasses-mk-one-carrier-card-one»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.ConjClasses_mk_one_carrier_card_eq_one
- «lem:count-primes-above-frob-sigma»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.count_primes_above_with_frobenius_eq_sigma
- «lem:cyclic-subgroup-trivial-meet»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.cyclic_subgroup_meets_G_times_one_trivially
- «lem:cyclotomic-density-two-sided»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.cyclotomic_density_from_two_sided_asymp
- «lem:cyclotomic-frobenius-norm-power»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.cyclotomic_frobenius_acts_as_norm_power
- «lem:dedekind-local-factor»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_local_factor_eq_product_artin_local
- «lem:density-S-sigma-tau»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH
- «lem:density-implies-lower»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.HasDirichletDensity.hasLower
- «lem:density-lift-fixedfield»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.density_lift_through_fixedField
- «lem:exists-frobenius-class»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.exists_frobeniusClass
- «lem:finite-ramified-primes»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.finite_ramifiedIn
- «lem:frobenius-class-eq-mk»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.frobeniusClass_eq_mk_of_isArithFrobAt
- «lem:has-density-finite»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.hasDirichletDensity_of_finite
- «lem:infinite-of-density-pos»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.infinite_of_hasDirichletDensity_pos
- «lem:liminf-ratio-ge-inv-card-G»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.liminf_ratio_ge_inv_card_G
- «lem:log-artin-asymp-character-sum»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.log_artinLSeries_asymp_character_sum
- «lem:logzeta-eq-loginv-bounded»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded
- «lem:logzeta-eq-primesum-bounded»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded
- «lem:pigeonhole-density»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one
- «lem:prime-ideal-sum-log»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_univ_tendsto_log
- «lem:prime-zeta-ge-log-minus-bounded»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.log_minus_bounded_le_primeIdealZetaSum
- «lem:prime-zeta-higher-tail-bounded»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaHigherTail_bounded
- «lem:prime-zeta-le-log-plus-bounded»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_le_log_plus_bounded
- «lem:primesum-fibre-asymp»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp
- «lem:ratio-glue-numerator»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_of_log_asymp_numerator
- «lem:ratiosum-fibres-tendsto-one»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.ratioSum_frobeniusFibres_tendsto_one
- «lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_one_of_log_pm_bounded
- «thm:chebotarev-abelian»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_abelian
- «thm:chebotarev-cyclotomic»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_cyclotomic
- «thm:chebotarev-density-comm»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_density_of_comm
- «thm:chebotarev-density»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.chebotarev_density
- «thm:dedekind-zeta-factorisation»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_eq_prod_artinDirichletSeries

Structure and coverage

Informal-only4Statements with no associated Lean code yet.

Ready to formalize1Entries whose next step is currently unblocked.

Formalized, ancestors open28Local Lean work is done, but prerequisite closure is still open.

Fully closed19Local code and ancestor closure are both complete.

Heaviest prerequisites (36)

«thm:chebotarev-abelian»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 5statement deps: 5proof deps: 3direct uses: 4downstream unlocks: 5
Associated lean decls (1)
- Chebotarev.chebotarev_abelian
«lem:primesum-fibre-asymp»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 3direct uses: 2downstream unlocks: 10
Associated lean decls (1)
- Chebotarev.primeIdealZetaSum_frobeniusFibre_asymp
«lem:density-lift-fixedfield»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 4statement deps: 4proof deps: 2direct uses: 2downstream unlocks: 4
Associated lean decls (1)
- Chebotarev.density_lift_through_fixedField
«cor:infinite-frobenius-class»(Corollary)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 3direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- Chebotarev.infinite_setOf_frobenius_class
«lem:cyclotomic-density-two-sided»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 3direct uses: 1downstream unlocks: 9
Associated lean decls (1)
- Chebotarev.cyclotomic_density_from_two_sided_asymp
«lem:prime-ideal-sum-log»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 3direct uses: 4downstream unlocks: 11
Associated lean decls (1)
- Chebotarev.primeIdealZetaSum_univ_tendsto_log
«thm:dedekind-zeta-factorisation»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 2direct uses: 1downstream unlocks: 12
Associated lean decls (1)
- Chebotarev.dedekindZeta_eq_prod_artinDirichletSeries
«lem:frobenius-class-eq-mk»(Lemma)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- Chebotarev.frobeniusClass_eq_mk_of_isArithFrobAt
«thm:chebotarev-cyclotomic»(Theorem)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 3statement deps: 3proof deps: 0direct uses: 1downstream unlocks: 8
Associated lean decls (1)
- Chebotarev.chebotarev_cyclotomic
«cor:density-split-completely»(Corollary)

Prerequisite fan-in measured from the current statement/proof dependency graph.

total deps: 2statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- Chebotarev.density_split_completely
Show all 26 more heaviest-prerequisite entries
- «lem:liminf-ratio-ge-inv-card-G»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - Chebotarev.liminf_ratio_ge_inv_card_G
- «lem:prime-zeta-ge-log-minus-bounded»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - Chebotarev.log_minus_bounded_le_primeIdealZetaSum
- «lem:prime-zeta-le-log-plus-bounded»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 12
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaSum_le_log_plus_bounded
- «thm:chebotarev-density-comm»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 2direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - Chebotarev.chebotarev_density_of_comm
- «thm:chebotarev-density»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 2direct uses: 5downstream unlocks: 3
  Associated lean decls (1)
  - Chebotarev.chebotarev_density
- «lem:ratiosum-fibres-tendsto-one»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 1direct uses: 2downstream unlocks: 6
  Associated lean decls (1)
  - Chebotarev.ratioSum_frobeniusFibres_tendsto_one
- «def:frobenius-at»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 26
- «lem:artin-analytic-extension»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 14
  Associated lean decls (1)
  - Chebotarev.artinLSeries_analytic_extension
- «lem:artin-euler-product-abelian»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 16
  Associated lean decls (1)
  - Chebotarev.exists_artinLSeries_eulerProduct_abelian
- «lem:character-orthogonality-eq»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_eq
- «lem:character-orthogonality-ne»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.character_orthogonality_cyclotomic_ne
- «lem:count-primes-above-frob-sigma»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (1)
  - Chebotarev.count_primes_above_with_frobenius_eq_sigma
- «lem:density-S-sigma-tau»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.liminf_density_S_sigma_ge_card_H_n_div_GH
- «lem:log-artin-asymp-character-sum»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 11
  Associated lean decls (1)
  - Chebotarev.log_artinLSeries_asymp_character_sum
- «lem:logzeta-eq-primesum-bounded»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 1direct uses: 4downstream unlocks: 14
  Associated lean decls (1)
  - Chebotarev.logDedekindZeta_sub_primeIdealZetaSum_bounded
- «cor:dirichlet-ap-density»(Corollary)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - Chebotarev.dirichlet_primes_in_AP
- «def:frobenius-class»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 10downstream unlocks: 23
  Associated lean decls (1)
  - Chebotarev.frobeniusClass
- «def:inertia-group»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
- «lem:H-n-over-H-tends-one»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.H_n_over_H_tends_to_one
- «lem:artin-one-ne-zero»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 13
  Associated lean decls (1)
  - Chebotarev.artinLSeries_one_ne_zero
- «lem:cyclotomic-frobenius-norm-power»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - Chebotarev.cyclotomic_frobenius_acts_as_norm_power
- «lem:dedekind-local-factor»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 13
  Associated lean decls (1)
  - Chebotarev.dedekindZeta_local_factor_eq_product_artin_local
- «lem:density-implies-lower»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - Chebotarev.HasDirichletDensity.hasLower
- «lem:exists-frobenius-class»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - Chebotarev.exists_frobeniusClass
- «lem:finite-ramified-primes»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 7
  Associated lean decls (1)
  - Chebotarev.finite_ramifiedIn
- «lem:has-density-finite»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - Chebotarev.hasDirichletDensity_of_finite

No prerequisites (16)

«def:unramified-in»(Definition)
Associated lean decls (1)
- Chebotarev.UnramifiedIn
«lem:character-sum-geom-numbers»(Lemma)
Associated lean decls (1)
- Chebotarev.character_sum_geometry_of_numbers_bound
«lem:conjclasses-mk-one-carrier-card-one»(Lemma)
Associated lean decls (1)
- Chebotarev.ConjClasses_mk_one_carrier_card_eq_one
«def:dirichlet-density»(Definition)
Associated lean decls (1)
- Chebotarev.HasDirichletDensity
«def:galois-character»(Definition)
Associated lean decls (1)
- Chebotarev.galoisCharacter
«lem:pigeonhole-density»(Lemma)
Associated lean decls (1)
- Chebotarev.tendsto_inv_card_of_liminf_ge_of_sum_tendsto_one
«lem:infinite-of-density-pos»(Lemma)
Associated lean decls (1)
- Chebotarev.infinite_of_hasDirichletDensity_pos
«lem:ratio-glue-numerator»(Lemma)
Associated lean decls (1)
- Chebotarev.tendsto_ratio_of_log_asymp_numerator
«def:decomposition-group»(Definition)
«lem:conjclasses-carrier-card-one-comm»(Lemma)
Associated lean decls (1)
- Chebotarev.ConjClasses_carrier_card_eq_one_of_comm
Show all 6 more entries without prerequisites
- «lem:prime-zeta-higher-tail-bounded»(Lemma)
  Associated lean decls (1)
  - Chebotarev.primeIdealZetaHigherTail_bounded
- «lem:cyclic-subgroup-trivial-meet»(Lemma)
  Associated lean decls (1)
  - Chebotarev.cyclic_subgroup_meets_G_times_one_trivially
- «lem:tendsto-ratio-one-of-log-pm-bounded»(Lemma)
  Associated lean decls (1)
  - Chebotarev.tendsto_ratio_one_of_log_pm_bounded
- «lem:logzeta-eq-loginv-bounded»(Lemma)
  Associated lean decls (1)
  - Chebotarev.logDedekindZeta_sub_log_inv_sub_one_bounded
- «lem:H-n-over-H-formula»(Lemma)
- «lem:conjclasses-carrier-card-pos»(Lemma)
  Associated lean decls (1)
  - Chebotarev.ConjClasses_carrier_card_pos

No dependents (9)

«thm:chebotarev-density-comm»(Theorem)
Associated lean decls (1)
- Chebotarev.chebotarev_density_of_comm
«lem:frobenius-class-eq-mk»(Lemma)
Associated lean decls (1)
- Chebotarev.frobeniusClass_eq_mk_of_isArithFrobAt
«def:inertia-group»(Definition)
«cor:density-split-completely»(Corollary)
Associated lean decls (1)
- Chebotarev.density_split_completely
«lem:cyclotomic-frobenius-norm-power»(Lemma)
Associated lean decls (1)
- Chebotarev.cyclotomic_frobenius_acts_as_norm_power
«cor:infinite-frobenius-class»(Corollary)
Associated lean decls (1)
- Chebotarev.infinite_setOf_frobenius_class
«lem:has-density-finite»(Lemma)
Associated lean decls (1)
- Chebotarev.hasDirichletDensity_of_finite
«lem:density-implies-lower»(Lemma)
Associated lean decls (1)
- Chebotarev.HasDirichletDensity.hasLower
«cor:dirichlet-ap-density»(Corollary)
Associated lean decls (1)
- Chebotarev.dirichlet_primes_in_AP