Blueprint Summary🔗

Overview

Total entries49completed: 49; deps incomplete: 0; sorries: 0; no proof: 0

Ready now0Entries whose next formalization step is currently unblocked.

Fully closed49Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Entry index (49)

Definitions11completed: 11; deps incomplete: 0; sorries: 0; no proof: 0

Lemmas18completed: 18; deps incomplete: 0; sorries: 0; no proof: 0

Theorems20completed: 20; deps incomplete: 0; sorries: 0; no proof: 0

Definition Index (11)

«def:fermat-number»(Definition)
Associated lean decls (1)
- Fermat
«def:saidak-sequence»(Definition)
Associated lean decls (1)
- a
«def:flt-nat»(Definition)
Associated lean decls (1)
- FermatLittleTheoremNat
«def:sqrt-two»(Definition)
Associated lean decls (1)
- IrrationalSqrtTwo
«def:cot-poly»(Definition)
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly
«def:flt»(Definition)
Associated lean decls (1)
- FermatLittleTheorem
«def:T»(Definition)
Associated lean decls (1)
- T
«def:sqrt-two-nat»(Definition)
Associated lean decls (1)
- IrrationalSqrtTwoNat
«def:inf-primes»(Definition)
Associated lean decls (1)
- InfinitudeOfPrimes
«def:basel»(Definition)
Associated lean decls (1)
- BaselProblem
«def:inf-primes-large»(Definition)
Associated lean decls (1)
- InfinitudeOfPrimes'

Theorem / Proposition / Lemma / Corollary Index (38)

«thm:inf-primes-goldbach»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Goldbach
«thm:inf-primes-euclid-factorial»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euclid
«lem:T-num-fp-eq»(Lemma)
Associated lean decls (1)
- T_num_fp_eq
«lem:saidak-primeFactors-card»(Lemma)
Associated lean decls (1)
- a_primeFactors_card_ge
«lem:fib-prime-ge-two»(Lemma)
Associated lean decls (1)
- fib_prime_ge_two
«thm:basel-cauchy»(Theorem)
Associated lean decls (1)
- BaselProblem.Cauchy.BaselProblem_Cauchy
«lem:fermat-recurrence»(Lemma)
Associated lean decls (1)
- Fermat_recurrence
«thm:inf-primes-euclid-prod-primes»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euclid'
«lem:T-comp-eq-mul»(Lemma)
Associated lean decls (1)
- T_comp_eq_mul
«thm:inf-primes-iff»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_iff_InfinitudeOfPrimes'
«lem:de-moivre»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.sin_two_mul_add_one
«thm:inf-primes-euler»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euler
«thm:flt-binomial»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem_Binomial
«lem:saidak-ge-two»(Lemma)
Associated lean decls (1)
- a_ge_two
«lem:cot-sq-lt-inv-sq»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.cotSq_lt_inv_sq
«lem:inv-sq-lt-csc-sq»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.inv_sq_lt_one_add_cotSq
«lem:fermat-ge-two»(Lemma)
Associated lean decls (1)
- Fermat_gt_two
«lem:fib-coprime-distinct-primes»(Lemma)
Associated lean decls (1)
- fib_coprime_of_distinct_primes
«thm:harmonic-unbounded»(Theorem)
Associated lean decls (1)
- harmonic_unbounded
«thm:basel-parseval»(Theorem)
Associated lean decls (1)
- BaselProblem.BaselProblem_Parseval
«thm:sqrt-two-valuation»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwo_Valuation
«thm:flt-nat-impl-flt»(Theorem)
Associated lean decls (1)
- FermatLittleTheoremNat_impl_FermatLittleTheorem
«thm:flt-alkauskas»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
«thm:inf-primes-saidak»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Saidak
«thm:flt-lagrange»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem_Lagrange
«lem:fermat-odd»(Lemma)
Associated lean decls (1)
- Fermat_odd
«thm:flt-dynamical»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem_Dynamical
«thm:inf-primes-wunderlich»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Wunderlich
«thm:sqrt-two-descent»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwo_Descent
«thm:sqrt-two-flt»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwo_FermatLastTheorem
«thm:sqrt-two-nat-impl-sqrt-two»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
«lem:fib-37-factorization»(Lemma)
Associated lean decls (1)
- fib_37
«lem:cot-poly-eval»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly_eval
«lem:cot-sq-sum»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.cotSq_sum
«lem:fermat-coprime»(Lemma)
Associated lean decls (1)
- Fermat_coprime
«thm:euler-prod-ge-harmonic»(Theorem)
Associated lean decls (1)
- prod_prime_div_prime_sub_one_ge_harmonic
«lem:flt-alkauskas-expansion»(Lemma)
Associated lean decls (1)
- FermatLittleTheorem.Alkauskas.exists_intExpansion
«lem:fermat-pairwise-coprime»(Lemma)
Associated lean decls (1)
- Fermat_pairwise_coprime

By parent groups (4)

Infinitude of primes. (19)

«lem:fermat-pairwise-coprime»(Lemma)
Associated lean decls (1)
- Fermat_pairwise_coprime
«thm:euler-prod-ge-harmonic»(Theorem)
Associated lean decls (1)
- prod_prime_div_prime_sub_one_ge_harmonic
«lem:fermat-coprime»(Lemma)
Associated lean decls (1)
- Fermat_coprime
«lem:fib-37-factorization»(Lemma)
Associated lean decls (1)
- fib_37
«thm:inf-primes-wunderlich»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Wunderlich
«lem:fermat-odd»(Lemma)
Associated lean decls (1)
- Fermat_odd
«thm:inf-primes-saidak»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Saidak
«thm:harmonic-unbounded»(Theorem)
Associated lean decls (1)
- harmonic_unbounded
«lem:fib-coprime-distinct-primes»(Lemma)
Associated lean decls (1)
- fib_coprime_of_distinct_primes
«lem:fermat-ge-two»(Lemma)
Associated lean decls (1)
- Fermat_gt_two
«lem:saidak-ge-two»(Lemma)
Associated lean decls (1)
- a_ge_two
«thm:inf-primes-euler»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euler
«thm:inf-primes-iff»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_iff_InfinitudeOfPrimes'
«thm:inf-primes-euclid-prod-primes»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euclid'
«lem:fermat-recurrence»(Lemma)
Associated lean decls (1)
- Fermat_recurrence
«lem:fib-prime-ge-two»(Lemma)
Associated lean decls (1)
- fib_prime_ge_two
«lem:saidak-primeFactors-card»(Lemma)
Associated lean decls (1)
- a_primeFactors_card_ge
«thm:inf-primes-euclid-factorial»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euclid
«thm:inf-primes-goldbach»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Goldbach

Fermat's Little Theorem. (8)

«lem:flt-alkauskas-expansion»(Lemma)
Associated lean decls (1)
- FermatLittleTheorem.Alkauskas.exists_intExpansion
«thm:flt-dynamical»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem_Dynamical
«thm:flt-lagrange»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem_Lagrange
«thm:flt-alkauskas»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
«thm:flt-nat-impl-flt»(Theorem)
Associated lean decls (1)
- FermatLittleTheoremNat_impl_FermatLittleTheorem
«thm:flt-binomial»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem_Binomial
«lem:T-comp-eq-mul»(Lemma)
Associated lean decls (1)
- T_comp_eq_mul
«lem:T-num-fp-eq»(Lemma)
Associated lean decls (1)
- T_num_fp_eq

Irrationality of square root of 2. (4)

«thm:sqrt-two-nat-impl-sqrt-two»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
«thm:sqrt-two-flt»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwo_FermatLastTheorem
«thm:sqrt-two-descent»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwo_Descent
«thm:sqrt-two-valuation»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwo_Valuation

Basel problem. (7)

«lem:cot-sq-sum»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.cotSq_sum
«lem:cot-poly-eval»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly_eval
«thm:basel-parseval»(Theorem)
Associated lean decls (1)
- BaselProblem.BaselProblem_Parseval
«lem:inv-sq-lt-csc-sq»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.inv_sq_lt_one_add_cotSq
«lem:cot-sq-lt-inv-sq»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.cotSq_lt_inv_sq
«lem:de-moivre»(Lemma)
Associated lean decls (1)
- BaselProblem.Cauchy.sin_two_mul_add_one
«thm:basel-cauchy»(Theorem)
Associated lean decls (1)
- BaselProblem.Cauchy.BaselProblem_Cauchy

Dependency insights

Statement-used entries16Entries reused in statement dependencies.

Proof-used entries19Entries reused in proof-only dependencies.

Tracked parent groups4Grouped health rollups for parents with more than one child entry.

Most used in statements (16)

«def:fermat-number»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 6
Associated lean decls (1)
- Fermat
«def:inf-primes»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 3
Associated lean decls (1)
- InfinitudeOfPrimes
«def:T»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- T
«def:saidak-sequence»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- a
«def:sqrt-two»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 4
Associated lean decls (1)
- IrrationalSqrtTwo
«def:flt-nat»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- FermatLittleTheoremNat
«def:flt»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- FermatLittleTheorem
«def:sqrt-two-nat»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- IrrationalSqrtTwoNat
«lem:fermat-odd»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- Fermat_odd
«lem:fermat-recurrence»(Lemma)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- Fermat_recurrence
Show all 6 more statement-used entries
- «thm:flt-nat-impl-flt»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 2
  Associated lean decls (1)
  - FermatLittleTheoremNat_impl_FermatLittleTheorem
- «lem:fermat-coprime»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - Fermat_coprime
- «lem:saidak-ge-two»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - a_ge_two
- «def:inf-primes-large»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - InfinitudeOfPrimes'
- «lem:T-comp-eq-mul»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - T_comp_eq_mul
- «lem:T-num-fp-eq»(Lemma)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - T_num_fp_eq

Most used in proofs (19)

«thm:flt-nat-impl-flt»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 2
Associated lean decls (1)
- FermatLittleTheoremNat_impl_FermatLittleTheorem
«def:basel»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- BaselProblem
«thm:sqrt-two-nat-impl-sqrt-two»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
«def:sqrt-two»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 4
Associated lean decls (1)
- IrrationalSqrtTwo
«def:inf-primes»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 3
Associated lean decls (1)
- InfinitudeOfPrimes
«def:cot-poly»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly
«lem:de-moivre»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
Associated lean decls (1)
- BaselProblem.Cauchy.sin_two_mul_add_one
«lem:cot-poly-eval»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly_eval
«lem:cot-sq-lt-inv-sq»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
- BaselProblem.Cauchy.cotSq_lt_inv_sq
«lem:cot-sq-sum»(Lemma)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
- BaselProblem.Cauchy.cotSq_sum
Show all 9 more proof-used entries
- «lem:fermat-pairwise-coprime»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - Fermat_pairwise_coprime
- «lem:fib-37-factorization»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - fib_37
- «lem:fib-coprime-distinct-primes»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - fib_coprime_of_distinct_primes
- «lem:fib-prime-ge-two»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - fib_prime_ge_two
- «lem:flt-alkauskas-expansion»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.exists_intExpansion
- «lem:inv-sq-lt-csc-sq»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - BaselProblem.Cauchy.inv_sq_lt_one_add_cotSq
- «lem:saidak-primeFactors-card»(Lemma)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - a_primeFactors_card_ge
- «thm:euler-prod-ge-harmonic»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - prod_prime_div_prime_sub_one_ge_harmonic
- «thm:harmonic-unbounded»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - harmonic_unbounded

Group health (4)

Infinitude of primes.«grp:inf-primes»

Grouped view over entries sharing the same parent.

total: 23closed: 23local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 30

Next: no ready child currently unlocks downstream work.
Fermat's Little Theorem.«grp:flt»

Grouped view over entries sharing the same parent.

total: 11closed: 11local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 14

Next: no ready child currently unlocks downstream work.
Basel problem.«grp:basel»

Grouped view over entries sharing the same parent.

total: 9closed: 9local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 13

Next: no ready child currently unlocks downstream work.
Irrationality of square root of 2.«grp:sqrt-two»

Grouped view over entries sharing the same parent.

total: 6closed: 6local-only: 0ready: 0blocked: 0incomplete Lean: 0unlock score: 9

Next: no ready child currently unlocks downstream work.

Metadata

Metadata audit

Missing owner49

Missing effort49

Untagged49

Missing owner (49)

«def:T»(Definition)

Missing owner metadata.
Associated lean decls (1)
- T
«def:basel»(Definition)

Missing owner metadata.
Associated lean decls (1)
- BaselProblem
«def:cot-poly»(Definition)

Missing owner metadata.
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly
«def:fermat-number»(Definition)

Missing owner metadata.
Associated lean decls (1)
- Fermat
«def:flt-nat»(Definition)

Missing owner metadata.
Associated lean decls (1)
- FermatLittleTheoremNat
«def:flt»(Definition)

Missing owner metadata.
Associated lean decls (1)
- FermatLittleTheorem
«def:inf-primes-large»(Definition)

Missing owner metadata.
Associated lean decls (1)
- InfinitudeOfPrimes'
«def:inf-primes»(Definition)

Missing owner metadata.
Associated lean decls (1)
- InfinitudeOfPrimes
«def:saidak-sequence»(Definition)

Missing owner metadata.
Associated lean decls (1)
- a
«def:sqrt-two-nat»(Definition)

Missing owner metadata.
Associated lean decls (1)
- IrrationalSqrtTwoNat
Show all 39 more entries missing owner
- «def:sqrt-two»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo
- «lem:T-comp-eq-mul»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - T_comp_eq_mul
- «lem:T-num-fp-eq»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - T_num_fp_eq
- «lem:cot-poly-eval»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotPoly_eval
- «lem:cot-sq-lt-inv-sq»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotSq_lt_inv_sq
- «lem:cot-sq-sum»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotSq_sum
- «lem:de-moivre»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.sin_two_mul_add_one
- «lem:fermat-coprime»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Fermat_coprime
- «lem:fermat-ge-two»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Fermat_gt_two
- «lem:fermat-odd»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Fermat_odd
- «lem:fermat-pairwise-coprime»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Fermat_pairwise_coprime
- «lem:fermat-recurrence»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - Fermat_recurrence
- «lem:fib-37-factorization»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - fib_37
- «lem:fib-coprime-distinct-primes»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - fib_coprime_of_distinct_primes
- «lem:fib-prime-ge-two»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - fib_prime_ge_two
- «lem:flt-alkauskas-expansion»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.exists_intExpansion
- «lem:inv-sq-lt-csc-sq»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.inv_sq_lt_one_add_cotSq
- «lem:saidak-ge-two»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - a_ge_two
- «lem:saidak-primeFactors-card»(Lemma)
  
  Missing owner metadata.
  Associated lean decls (1)
  - a_primeFactors_card_ge
- «thm:basel-cauchy»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.BaselProblem_Cauchy
- «thm:basel-parseval»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - BaselProblem.BaselProblem_Parseval
- «thm:euler-prod-ge-harmonic»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - prod_prime_div_prime_sub_one_ge_harmonic
- «thm:flt-alkauskas»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
- «thm:flt-binomial»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Binomial
- «thm:flt-dynamical»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Dynamical
- «thm:flt-lagrange»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Lagrange
- «thm:flt-nat-impl-flt»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - FermatLittleTheoremNat_impl_FermatLittleTheorem
- «thm:harmonic-unbounded»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - harmonic_unbounded
- «thm:inf-primes-euclid-factorial»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euclid
- «thm:inf-primes-euclid-prod-primes»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euclid'
- «thm:inf-primes-euler»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euler
- «thm:inf-primes-goldbach»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Goldbach
- «thm:inf-primes-iff»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_iff_InfinitudeOfPrimes'
- «thm:inf-primes-saidak»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Saidak
- «thm:inf-primes-wunderlich»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Wunderlich
- «thm:sqrt-two-descent»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_Descent
- «thm:sqrt-two-flt»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_FermatLastTheorem
- «thm:sqrt-two-nat-impl-sqrt-two»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
- «thm:sqrt-two-valuation»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_Valuation

Missing effort (49)

«def:T»(Definition)

Missing effort metadata.
Associated lean decls (1)
- T
«def:basel»(Definition)

Missing effort metadata.
Associated lean decls (1)
- BaselProblem
«def:cot-poly»(Definition)

Missing effort metadata.
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly
«def:fermat-number»(Definition)

Missing effort metadata.
Associated lean decls (1)
- Fermat
«def:flt-nat»(Definition)

Missing effort metadata.
Associated lean decls (1)
- FermatLittleTheoremNat
«def:flt»(Definition)

Missing effort metadata.
Associated lean decls (1)
- FermatLittleTheorem
«def:inf-primes-large»(Definition)

Missing effort metadata.
Associated lean decls (1)
- InfinitudeOfPrimes'
«def:inf-primes»(Definition)

Missing effort metadata.
Associated lean decls (1)
- InfinitudeOfPrimes
«def:saidak-sequence»(Definition)

Missing effort metadata.
Associated lean decls (1)
- a
«def:sqrt-two-nat»(Definition)

Missing effort metadata.
Associated lean decls (1)
- IrrationalSqrtTwoNat
Show all 39 more entries missing effort
- «def:sqrt-two»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo
- «lem:T-comp-eq-mul»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - T_comp_eq_mul
- «lem:T-num-fp-eq»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - T_num_fp_eq
- «lem:cot-poly-eval»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotPoly_eval
- «lem:cot-sq-lt-inv-sq»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotSq_lt_inv_sq
- «lem:cot-sq-sum»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotSq_sum
- «lem:de-moivre»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.sin_two_mul_add_one
- «lem:fermat-coprime»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Fermat_coprime
- «lem:fermat-ge-two»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Fermat_gt_two
- «lem:fermat-odd»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Fermat_odd
- «lem:fermat-pairwise-coprime»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Fermat_pairwise_coprime
- «lem:fermat-recurrence»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - Fermat_recurrence
- «lem:fib-37-factorization»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - fib_37
- «lem:fib-coprime-distinct-primes»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - fib_coprime_of_distinct_primes
- «lem:fib-prime-ge-two»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - fib_prime_ge_two
- «lem:flt-alkauskas-expansion»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.exists_intExpansion
- «lem:inv-sq-lt-csc-sq»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.inv_sq_lt_one_add_cotSq
- «lem:saidak-ge-two»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - a_ge_two
- «lem:saidak-primeFactors-card»(Lemma)
  
  Missing effort metadata.
  Associated lean decls (1)
  - a_primeFactors_card_ge
- «thm:basel-cauchy»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.BaselProblem_Cauchy
- «thm:basel-parseval»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - BaselProblem.BaselProblem_Parseval
- «thm:euler-prod-ge-harmonic»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - prod_prime_div_prime_sub_one_ge_harmonic
- «thm:flt-alkauskas»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
- «thm:flt-binomial»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Binomial
- «thm:flt-dynamical»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Dynamical
- «thm:flt-lagrange»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Lagrange
- «thm:flt-nat-impl-flt»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - FermatLittleTheoremNat_impl_FermatLittleTheorem
- «thm:harmonic-unbounded»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - harmonic_unbounded
- «thm:inf-primes-euclid-factorial»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euclid
- «thm:inf-primes-euclid-prod-primes»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euclid'
- «thm:inf-primes-euler»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euler
- «thm:inf-primes-goldbach»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Goldbach
- «thm:inf-primes-iff»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_iff_InfinitudeOfPrimes'
- «thm:inf-primes-saidak»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Saidak
- «thm:inf-primes-wunderlich»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Wunderlich
- «thm:sqrt-two-descent»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_Descent
- «thm:sqrt-two-flt»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_FermatLastTheorem
- «thm:sqrt-two-nat-impl-sqrt-two»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
- «thm:sqrt-two-valuation»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_Valuation

Untagged (49)

«def:T»(Definition)

Missing tag metadata.
Associated lean decls (1)
- T
«def:basel»(Definition)

Missing tag metadata.
Associated lean decls (1)
- BaselProblem
«def:cot-poly»(Definition)

Missing tag metadata.
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly
«def:fermat-number»(Definition)

Missing tag metadata.
Associated lean decls (1)
- Fermat
«def:flt-nat»(Definition)

Missing tag metadata.
Associated lean decls (1)
- FermatLittleTheoremNat
«def:flt»(Definition)

Missing tag metadata.
Associated lean decls (1)
- FermatLittleTheorem
«def:inf-primes-large»(Definition)

Missing tag metadata.
Associated lean decls (1)
- InfinitudeOfPrimes'
«def:inf-primes»(Definition)

Missing tag metadata.
Associated lean decls (1)
- InfinitudeOfPrimes
«def:saidak-sequence»(Definition)

Missing tag metadata.
Associated lean decls (1)
- a
«def:sqrt-two-nat»(Definition)

Missing tag metadata.
Associated lean decls (1)
- IrrationalSqrtTwoNat
Show all 39 more untagged entries
- «def:sqrt-two»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo
- «lem:T-comp-eq-mul»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - T_comp_eq_mul
- «lem:T-num-fp-eq»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - T_num_fp_eq
- «lem:cot-poly-eval»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotPoly_eval
- «lem:cot-sq-lt-inv-sq»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotSq_lt_inv_sq
- «lem:cot-sq-sum»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotSq_sum
- «lem:de-moivre»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.sin_two_mul_add_one
- «lem:fermat-coprime»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Fermat_coprime
- «lem:fermat-ge-two»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Fermat_gt_two
- «lem:fermat-odd»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Fermat_odd
- «lem:fermat-pairwise-coprime»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Fermat_pairwise_coprime
- «lem:fermat-recurrence»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - Fermat_recurrence
- «lem:fib-37-factorization»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - fib_37
- «lem:fib-coprime-distinct-primes»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - fib_coprime_of_distinct_primes
- «lem:fib-prime-ge-two»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - fib_prime_ge_two
- «lem:flt-alkauskas-expansion»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.exists_intExpansion
- «lem:inv-sq-lt-csc-sq»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.inv_sq_lt_one_add_cotSq
- «lem:saidak-ge-two»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - a_ge_two
- «lem:saidak-primeFactors-card»(Lemma)
  
  Missing tag metadata.
  Associated lean decls (1)
  - a_primeFactors_card_ge
- «thm:basel-cauchy»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - BaselProblem.Cauchy.BaselProblem_Cauchy
- «thm:basel-parseval»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - BaselProblem.BaselProblem_Parseval
- «thm:euler-prod-ge-harmonic»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - prod_prime_div_prime_sub_one_ge_harmonic
- «thm:flt-alkauskas»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
- «thm:flt-binomial»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Binomial
- «thm:flt-dynamical»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Dynamical
- «thm:flt-lagrange»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FermatLittleTheorem_Lagrange
- «thm:flt-nat-impl-flt»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - FermatLittleTheoremNat_impl_FermatLittleTheorem
- «thm:harmonic-unbounded»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - harmonic_unbounded
- «thm:inf-primes-euclid-factorial»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euclid
- «thm:inf-primes-euclid-prod-primes»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euclid'
- «thm:inf-primes-euler»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euler
- «thm:inf-primes-goldbach»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Goldbach
- «thm:inf-primes-iff»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_iff_InfinitudeOfPrimes'
- «thm:inf-primes-saidak»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Saidak
- «thm:inf-primes-wunderlich»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - InfinitudeOfPrimes_Wunderlich
- «thm:sqrt-two-descent»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_Descent
- «thm:sqrt-two-flt»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_FermatLastTheorem
- «thm:sqrt-two-nat-impl-sqrt-two»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
- «thm:sqrt-two-valuation»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - IrrationalSqrtTwo_Valuation

Structure and coverage

Fully closed49Local code and ancestor closure are both complete.

Heaviest prerequisites (27)

«thm:basel-cauchy»(Theorem)

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

total deps: 4statement deps: 0proof deps: 4direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- BaselProblem.Cauchy.BaselProblem_Cauchy
«thm:inf-primes-wunderlich»(Theorem)

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

total deps: 3statement deps: 0proof deps: 3direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- InfinitudeOfPrimes_Wunderlich
«thm:flt-dynamical»(Theorem)

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)
- FermatLittleTheorem_Dynamical
«lem:cot-poly-eval»(Lemma)

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

total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly_eval
«thm:flt-alkauskas»(Theorem)

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

total deps: 2statement deps: 0proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
«thm:inf-primes-euler»(Theorem)

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

total deps: 2statement deps: 0proof deps: 2direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- InfinitudeOfPrimes_Euler
«lem:fermat-coprime»(Lemma)

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

total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 2
Associated lean decls (1)
- Fermat_coprime
«lem:saidak-primeFactors-card»(Lemma)

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

total deps: 2statement deps: 2proof deps: 0direct uses: 1downstream unlocks: 1
Associated lean decls (1)
- a_primeFactors_card_ge
«thm:flt-nat-impl-flt»(Theorem)

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

total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 2
Associated lean decls (1)
- FermatLittleTheoremNat_impl_FermatLittleTheorem
«thm:inf-primes-iff»(Theorem)

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

total deps: 2statement deps: 2proof deps: 0direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- InfinitudeOfPrimes_iff_InfinitudeOfPrimes'
Show all 17 more heaviest-prerequisite entries
- «thm:sqrt-two-nat-impl-sqrt-two»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - IrrationalSqrtTwoNat_impl_IrrationalSqrtTwo
- «lem:cot-sq-sum»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotSq_sum
- «thm:basel-parseval»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - BaselProblem.BaselProblem_Parseval
- «thm:inf-primes-euclid-factorial»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - InfinitudeOfPrimes_Euclid
- «thm:inf-primes-goldbach»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - InfinitudeOfPrimes_Goldbach
- «thm:inf-primes-saidak»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - InfinitudeOfPrimes_Saidak
- «thm:sqrt-two-descent»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - IrrationalSqrtTwo_Descent
- «thm:sqrt-two-flt»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - IrrationalSqrtTwo_FermatLastTheorem
- «thm:sqrt-two-valuation»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 0downstream unlocks: 0
  Associated lean decls (1)
  - IrrationalSqrtTwo_Valuation
- «lem:T-comp-eq-mul»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - T_comp_eq_mul
- «lem:T-num-fp-eq»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - T_num_fp_eq
- «lem:fermat-ge-two»(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)
  - Fermat_gt_two
- «lem:fermat-odd»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Fermat_odd
- «lem:fermat-pairwise-coprime»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (1)
  - Fermat_pairwise_coprime
- «lem:fermat-recurrence»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - Fermat_recurrence
- «lem:saidak-ge-two»(Lemma)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - a_ge_two
- «thm:inf-primes-euclid-prod-primes»(Theorem)
  
  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)
  - InfinitudeOfPrimes_Euclid'

No prerequisites (22)

«lem:fib-prime-ge-two»(Lemma)
Associated lean decls (1)
- fib_prime_ge_two
«thm:flt-binomial»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem_Binomial
«lem:fib-coprime-distinct-primes»(Lemma)
Associated lean decls (1)
- fib_coprime_of_distinct_primes
«thm:harmonic-unbounded»(Theorem)
Associated lean decls (1)
- harmonic_unbounded
«def:sqrt-two»(Definition)
Associated lean decls (1)
- IrrationalSqrtTwo
«def:cot-poly»(Definition)
Associated lean decls (1)
- BaselProblem.Cauchy.cotPoly
«def:flt»(Definition)
Associated lean decls (1)
- FermatLittleTheorem
«def:T»(Definition)
Associated lean decls (1)
- T
«def:sqrt-two-nat»(Definition)
Associated lean decls (1)
- IrrationalSqrtTwoNat
«thm:euler-prod-ge-harmonic»(Theorem)
Associated lean decls (1)
- prod_prime_div_prime_sub_one_ge_harmonic
Show all 12 more entries without prerequisites
- «def:inf-primes»(Definition)
  Associated lean decls (1)
  - InfinitudeOfPrimes
- «def:basel»(Definition)
  Associated lean decls (1)
  - BaselProblem
- «lem:flt-alkauskas-expansion»(Lemma)
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.exists_intExpansion
- «def:inf-primes-large»(Definition)
  Associated lean decls (1)
  - InfinitudeOfPrimes'
- «lem:fib-37-factorization»(Lemma)
  Associated lean decls (1)
  - fib_37
- «thm:flt-lagrange»(Theorem)
  Associated lean decls (1)
  - FermatLittleTheorem_Lagrange
- «lem:inv-sq-lt-csc-sq»(Lemma)
  Associated lean decls (1)
  - BaselProblem.Cauchy.inv_sq_lt_one_add_cotSq
- «lem:cot-sq-lt-inv-sq»(Lemma)
  Associated lean decls (1)
  - BaselProblem.Cauchy.cotSq_lt_inv_sq
- «def:flt-nat»(Definition)
  Associated lean decls (1)
  - FermatLittleTheoremNat
- «def:saidak-sequence»(Definition)
  Associated lean decls (1)
  - a
- «lem:de-moivre»(Lemma)
  Associated lean decls (1)
  - BaselProblem.Cauchy.sin_two_mul_add_one
- «def:fermat-number»(Definition)
  Associated lean decls (1)
  - Fermat

No dependents (17)

«thm:inf-primes-goldbach»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Goldbach
«thm:inf-primes-euclid-factorial»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euclid
«thm:inf-primes-euclid-prod-primes»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euclid'
«thm:inf-primes-iff»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_iff_InfinitudeOfPrimes'
«thm:inf-primes-euler»(Theorem)
Associated lean decls (1)
- InfinitudeOfPrimes_Euler
«thm:flt-binomial»(Theorem)
Associated lean decls (1)
- FermatLittleTheorem_Binomial
«lem:fermat-ge-two»(Lemma)
Associated lean decls (1)
- Fermat_gt_two
«thm:basel-parseval»(Theorem)
Associated lean decls (1)
- BaselProblem.BaselProblem_Parseval
«thm:sqrt-two-valuation»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwo_Valuation
«thm:sqrt-two-flt»(Theorem)
Associated lean decls (1)
- IrrationalSqrtTwo_FermatLastTheorem
Show all 7 more entries without dependents
- «thm:sqrt-two-descent»(Theorem)
  Associated lean decls (1)
  - IrrationalSqrtTwo_Descent
- «thm:inf-primes-wunderlich»(Theorem)
  Associated lean decls (1)
  - InfinitudeOfPrimes_Wunderlich
- «thm:flt-dynamical»(Theorem)
  Associated lean decls (1)
  - FermatLittleTheorem_Dynamical
- «thm:flt-lagrange»(Theorem)
  Associated lean decls (1)
  - FermatLittleTheorem_Lagrange
- «thm:inf-primes-saidak»(Theorem)
  Associated lean decls (1)
  - InfinitudeOfPrimes_Saidak
- «thm:flt-alkauskas»(Theorem)
  Associated lean decls (1)
  - FermatLittleTheorem.Alkauskas.FermatLittleTheorem_Alkauskas
- «thm:basel-cauchy»(Theorem)
  Associated lean decls (1)
  - BaselProblem.Cauchy.BaselProblem_Cauchy