Blueprint Summary🔗

Overview

Total entries30completed: 30; deps incomplete: 0; sorries: 0; no proof: 0

Ready now0Entries whose next formalization step is currently unblocked.

Fully closed30Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Entry index (30)

Definitions6completed: 6; deps incomplete: 0; sorries: 0; no proof: 0

Theorems24completed: 24; deps incomplete: 0; sorries: 0; no proof: 0

Definition Index (6)

«frobenius-degree»(Definition)
Associated lean decls (2)
- HasseWeil.frobeniusIsog_degree
- HasseWeil.frobenius_finrank_functionField
«frobenius-isogeny»(Definition)
Associated lean decls (2)
- HasseWeil.frobeniusIsog
- HasseWeil.frobeniusIsog_pullback_apply
isogeny(Definition)
Associated lean decls (2)
- HasseWeil.Isogeny
- HasseWeil.Isogeny.degree
«dual-isogeny»(Definition)
Associated lean decls (2)
- HasseWeil.IsDualOf
- HasseWeil.degree_dual_of_witness
«isog-trace»(Definition)
Associated lean decls (1)
- HasseWeil.isogTrace
«point-count»(Definition)
Associated lean decls (1)
- HasseWeil.pointCount

Theorem / Proposition / Lemma / Corollary Index (24)

«hasse-bound-weil-capstone»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.hasse_bound_via_weil_pairing
- HasseWeil.WeilPairing.hasse_bound_unconditional_of_baseChange_scalings_coprime
«mul-by-n-trace»(Theorem)
Associated lean decls (1)
- HasseWeil.isogTrace_mulByInt
«trace-sq-le-four-q»(Theorem)
Associated lean decls (1)
- HasseWeil.trace_sq_le_four_mul_deg
«hasse-bound-from-witnesses»(Theorem)
Associated lean decls (2)
- HasseWeil.hasse_bound_of_qf_nonneg_witnesses
- HasseWeil.hasse_bound_of_full_qf_nonneg_witnesses
«dual-additivity»(Theorem)
Associated lean decls (2)
- HasseWeil.dual_add_of_trace_witnesses
- HasseWeil.dual_add_of_sum_witnesses
«degree-quadratic-scalar»(Theorem)
Associated lean decls (1)
- HasseWeil.degree_quadratic_mulByInt
«mul-by-n-degree»(Theorem)
Associated lean decls (2)
- HasseWeil.mulByInt
- HasseWeil.mulByInt_degree
«one-sub-frobenius-separable»(Theorem)
Associated lean decls (2)
- HasseWeil.oneSubFrobenius_isSeparable_of_witness
- HasseWeil.isSeparable_iff_of_coeff_witness
«degree-nonneg»(Theorem)
Associated lean decls (2)
- HasseWeil.qf_nonneg_of_genuine_chain
- HasseWeil.degree_quadratic_mulByInt_nonneg
«frobenius-fixed-locus»(Theorem)
Associated lean decls (2)
- HasseWeil.frobenius_fixed_iff_mem_baseField
- HasseWeil.range_algebraMap_eq_roots_X_pow_card_sub_X
«hasse-bound»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.hasse_bound
- HasseWeil.WeilPairing.hasse_bound_unconditional
«frob-det-data»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.TorsionGeometric.frob_det_residual_of_weil_scaling
- HasseWeil.WeilPairing.frob_det_residual_baseChange
«matrix-det-quadratic»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.det_smul_sub_smul_one_fin_two
- HasseWeil.WeilPairing.det_one_sub_fin_two
«pointcount-eq-trace»(Theorem)
Associated lean decls (2)
- HasseWeil.pointCount_eq_of_witness
- HasseWeil.pointCount_eq_of_hom_kernel_witness
«qf-coprime-to-all»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime
- HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime_both
«degree-multiplicative»(Theorem)
Associated lean decls (2)
- HasseWeil.Isogeny.comp_degree
- HasseWeil.Isogeny.comp_degree_pos
«kernel-card-degree»(Theorem)
Associated lean decls (2)
- HasseWeil.Isogeny.card_kernel_eq_degree_of_separable_witness
- HasseWeil.card_kernel_eq_degree_of_separable_coordHom
«sum-trace-frobenius»(Theorem)
Associated lean decls (2)
- HasseWeil.sum_trace_frobenius_witness
- HasseWeil.dual_comp_frobenius_witness
«degree-quadratic-form»(Theorem)
Associated lean decls (1)
- HasseWeil.traceOfFrobenius_sq_le_of_qf_nonneg
«degree-quadratic-polarisation»(Theorem)
Associated lean decls (1)
- HasseWeil.degree_quadratic_genuine_addIsog
«deg-one-sub-pi-eq-pointcount»(Theorem)
Associated lean decls (2)
- HasseWeil.isogOneSub_negFrobenius_degree_eq_pointCount
- HasseWeil.kernel_eq_top_of_hom_eq_id_sub_frobenius
«sqrt-bound»(Theorem)
Associated lean decls (1)
- HasseWeil.abs_le_two_sqrt_of_sq_le
«det-deg»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.TorsionGeometric.det_rhoEll_eq_degree
- HasseWeil.WeilPairing.TorsionGeometric.linearMap_det_torsionRestrict_eq
«qf-nonneg-weil»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data
- HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data_both

Dependency insights

Statement-used entries10Entries reused in statement dependencies.

Proof-used entries25Entries reused in proof-only dependencies.

Most used in statements (10)

«frobenius-isogeny»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 2direct uses: 5downstream unlocks: 19
Associated lean decls (2)
- HasseWeil.frobeniusIsog
- HasseWeil.frobeniusIsog_pullback_apply
isogeny(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 11
Associated lean decls (2)
- HasseWeil.Isogeny
- HasseWeil.Isogeny.degree
«mul-by-n-degree»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 10
Associated lean decls (2)
- HasseWeil.mulByInt
- HasseWeil.mulByInt_degree
«point-count»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 20
Associated lean decls (1)
- HasseWeil.pointCount
«isog-trace»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 11
Associated lean decls (1)
- HasseWeil.isogTrace
«dual-isogeny»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 6
Associated lean decls (2)
- HasseWeil.IsDualOf
- HasseWeil.degree_dual_of_witness
«frobenius-fixed-locus»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 4
Associated lean decls (2)
- HasseWeil.frobenius_fixed_iff_mem_baseField
- HasseWeil.range_algebraMap_eq_roots_X_pow_card_sub_X
«degree-quadratic-polarisation»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- HasseWeil.degree_quadratic_genuine_addIsog
«pointcount-eq-trace»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 2
Associated lean decls (2)
- HasseWeil.pointCount_eq_of_witness
- HasseWeil.pointCount_eq_of_hom_kernel_witness
«degree-nonneg»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 0direct uses: 1downstream unlocks: 2
Associated lean decls (2)
- HasseWeil.qf_nonneg_of_genuine_chain
- HasseWeil.degree_quadratic_mulByInt_nonneg

Most used in proofs (25)

«frobenius-degree»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 8
Associated lean decls (2)
- HasseWeil.frobeniusIsog_degree
- HasseWeil.frobenius_finrank_functionField
«trace-sq-le-four-q»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 4statement uses: 0direct uses: 4downstream unlocks: 7
Associated lean decls (1)
- HasseWeil.trace_sq_le_four_mul_deg
«frobenius-isogeny»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 3direct uses: 5downstream unlocks: 19
Associated lean decls (2)
- HasseWeil.frobeniusIsog
- HasseWeil.frobeniusIsog_pullback_apply
«mul-by-n-trace»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 10
Associated lean decls (1)
- HasseWeil.isogTrace_mulByInt
«dual-additivity»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 5
Associated lean decls (2)
- HasseWeil.dual_add_of_trace_witnesses
- HasseWeil.dual_add_of_sum_witnesses
«sqrt-bound»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- HasseWeil.abs_le_two_sqrt_of_sq_le
«pointcount-eq-trace»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 2
Associated lean decls (2)
- HasseWeil.pointCount_eq_of_witness
- HasseWeil.pointCount_eq_of_hom_kernel_witness
«point-count»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 20
Associated lean decls (1)
- HasseWeil.pointCount
isogeny(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 11
Associated lean decls (2)
- HasseWeil.Isogeny
- HasseWeil.Isogeny.degree
«isog-trace»(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 11
Associated lean decls (1)
- HasseWeil.isogTrace
Show all 15 more proof-used entries
- «mul-by-n-degree»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 10
  Associated lean decls (2)
  - HasseWeil.mulByInt
  - HasseWeil.mulByInt_degree
- «dual-isogeny»(Definition)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 6
  Associated lean decls (2)
  - HasseWeil.IsDualOf
  - HasseWeil.degree_dual_of_witness
- «kernel-card-degree»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - HasseWeil.Isogeny.card_kernel_eq_degree_of_separable_witness
  - HasseWeil.card_kernel_eq_degree_of_separable_coordHom
- «one-sub-frobenius-separable»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - HasseWeil.oneSubFrobenius_isSeparable_of_witness
  - HasseWeil.isSeparable_iff_of_coeff_witness
- «sum-trace-frobenius»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - HasseWeil.sum_trace_frobenius_witness
  - HasseWeil.dual_comp_frobenius_witness
- «degree-quadratic-polarisation»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - HasseWeil.degree_quadratic_genuine_addIsog
- «deg-one-sub-pi-eq-pointcount»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - HasseWeil.isogOneSub_negFrobenius_degree_eq_pointCount
  - HasseWeil.kernel_eq_top_of_hom_eq_id_sub_frobenius
- «det-deg»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - HasseWeil.WeilPairing.TorsionGeometric.det_rhoEll_eq_degree
  - HasseWeil.WeilPairing.TorsionGeometric.linearMap_det_torsionRestrict_eq
- «matrix-det-quadratic»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (2)
  - HasseWeil.WeilPairing.det_smul_sub_smul_one_fin_two
  - HasseWeil.WeilPairing.det_one_sub_fin_two
- «degree-quadratic-form»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - HasseWeil.traceOfFrobenius_sq_le_of_qf_nonneg
- «frob-det-data»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - HasseWeil.WeilPairing.TorsionGeometric.frob_det_residual_of_weil_scaling
  - HasseWeil.WeilPairing.frob_det_residual_baseChange
- «qf-coprime-to-all»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime_both
- «hasse-bound-from-witnesses»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - HasseWeil.hasse_bound_of_qf_nonneg_witnesses
  - HasseWeil.hasse_bound_of_full_qf_nonneg_witnesses
- «hasse-bound»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - HasseWeil.WeilPairing.hasse_bound
  - HasseWeil.WeilPairing.hasse_bound_unconditional
- «qf-nonneg-weil»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data_both

Metadata

Metadata audit

Missing owner30

Missing effort30

Untagged30

Missing owner (30)

isogeny(Definition)

Missing owner metadata.
Associated lean decls (2)
- HasseWeil.Isogeny
- HasseWeil.Isogeny.degree
«deg-one-sub-pi-eq-pointcount»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- HasseWeil.isogOneSub_negFrobenius_degree_eq_pointCount
- HasseWeil.kernel_eq_top_of_hom_eq_id_sub_frobenius
«degree-multiplicative»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- HasseWeil.Isogeny.comp_degree
- HasseWeil.Isogeny.comp_degree_pos
«degree-nonneg»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- HasseWeil.qf_nonneg_of_genuine_chain
- HasseWeil.degree_quadratic_mulByInt_nonneg
«degree-quadratic-form»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- HasseWeil.traceOfFrobenius_sq_le_of_qf_nonneg
«degree-quadratic-polarisation»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- HasseWeil.degree_quadratic_genuine_addIsog
«degree-quadratic-scalar»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- HasseWeil.degree_quadratic_mulByInt
«det-deg»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- HasseWeil.WeilPairing.TorsionGeometric.det_rhoEll_eq_degree
- HasseWeil.WeilPairing.TorsionGeometric.linearMap_det_torsionRestrict_eq
«dual-additivity»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- HasseWeil.dual_add_of_trace_witnesses
- HasseWeil.dual_add_of_sum_witnesses
«dual-isogeny»(Definition)

Missing owner metadata.
Associated lean decls (2)
- HasseWeil.IsDualOf
- HasseWeil.degree_dual_of_witness
Show all 20 more entries missing owner
- «frob-det-data»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.TorsionGeometric.frob_det_residual_of_weil_scaling
  - HasseWeil.WeilPairing.frob_det_residual_baseChange
- «frobenius-degree»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.frobeniusIsog_degree
  - HasseWeil.frobenius_finrank_functionField
- «frobenius-fixed-locus»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.frobenius_fixed_iff_mem_baseField
  - HasseWeil.range_algebraMap_eq_roots_X_pow_card_sub_X
- «frobenius-isogeny»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.frobeniusIsog
  - HasseWeil.frobeniusIsog_pullback_apply
- «hasse-bound-from-witnesses»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.hasse_bound_of_qf_nonneg_witnesses
  - HasseWeil.hasse_bound_of_full_qf_nonneg_witnesses
- «hasse-bound-weil-capstone»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.hasse_bound_via_weil_pairing
  - HasseWeil.WeilPairing.hasse_bound_unconditional_of_baseChange_scalings_coprime
- «hasse-bound»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.hasse_bound
  - HasseWeil.WeilPairing.hasse_bound_unconditional
- «isog-trace»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HasseWeil.isogTrace
- «kernel-card-degree»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.Isogeny.card_kernel_eq_degree_of_separable_witness
  - HasseWeil.card_kernel_eq_degree_of_separable_coordHom
- «matrix-det-quadratic»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.det_smul_sub_smul_one_fin_two
  - HasseWeil.WeilPairing.det_one_sub_fin_two
- «mul-by-n-degree»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.mulByInt
  - HasseWeil.mulByInt_degree
- «mul-by-n-trace»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HasseWeil.isogTrace_mulByInt
- «one-sub-frobenius-separable»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.oneSubFrobenius_isSeparable_of_witness
  - HasseWeil.isSeparable_iff_of_coeff_witness
- «point-count»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HasseWeil.pointCount
- «pointcount-eq-trace»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.pointCount_eq_of_witness
  - HasseWeil.pointCount_eq_of_hom_kernel_witness
- «qf-coprime-to-all»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime_both
- «qf-nonneg-weil»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data_both
- «sqrt-bound»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HasseWeil.abs_le_two_sqrt_of_sq_le
- «sum-trace-frobenius»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HasseWeil.sum_trace_frobenius_witness
  - HasseWeil.dual_comp_frobenius_witness
- «trace-sq-le-four-q»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HasseWeil.trace_sq_le_four_mul_deg

Missing effort (30)

isogeny(Definition)

Missing effort metadata.
Associated lean decls (2)
- HasseWeil.Isogeny
- HasseWeil.Isogeny.degree
«deg-one-sub-pi-eq-pointcount»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- HasseWeil.isogOneSub_negFrobenius_degree_eq_pointCount
- HasseWeil.kernel_eq_top_of_hom_eq_id_sub_frobenius
«degree-multiplicative»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- HasseWeil.Isogeny.comp_degree
- HasseWeil.Isogeny.comp_degree_pos
«degree-nonneg»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- HasseWeil.qf_nonneg_of_genuine_chain
- HasseWeil.degree_quadratic_mulByInt_nonneg
«degree-quadratic-form»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- HasseWeil.traceOfFrobenius_sq_le_of_qf_nonneg
«degree-quadratic-polarisation»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- HasseWeil.degree_quadratic_genuine_addIsog
«degree-quadratic-scalar»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- HasseWeil.degree_quadratic_mulByInt
«det-deg»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- HasseWeil.WeilPairing.TorsionGeometric.det_rhoEll_eq_degree
- HasseWeil.WeilPairing.TorsionGeometric.linearMap_det_torsionRestrict_eq
«dual-additivity»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- HasseWeil.dual_add_of_trace_witnesses
- HasseWeil.dual_add_of_sum_witnesses
«dual-isogeny»(Definition)

Missing effort metadata.
Associated lean decls (2)
- HasseWeil.IsDualOf
- HasseWeil.degree_dual_of_witness
Show all 20 more entries missing effort
- «frob-det-data»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.TorsionGeometric.frob_det_residual_of_weil_scaling
  - HasseWeil.WeilPairing.frob_det_residual_baseChange
- «frobenius-degree»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.frobeniusIsog_degree
  - HasseWeil.frobenius_finrank_functionField
- «frobenius-fixed-locus»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.frobenius_fixed_iff_mem_baseField
  - HasseWeil.range_algebraMap_eq_roots_X_pow_card_sub_X
- «frobenius-isogeny»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.frobeniusIsog
  - HasseWeil.frobeniusIsog_pullback_apply
- «hasse-bound-from-witnesses»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.hasse_bound_of_qf_nonneg_witnesses
  - HasseWeil.hasse_bound_of_full_qf_nonneg_witnesses
- «hasse-bound-weil-capstone»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.hasse_bound_via_weil_pairing
  - HasseWeil.WeilPairing.hasse_bound_unconditional_of_baseChange_scalings_coprime
- «hasse-bound»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.hasse_bound
  - HasseWeil.WeilPairing.hasse_bound_unconditional
- «isog-trace»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HasseWeil.isogTrace
- «kernel-card-degree»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.Isogeny.card_kernel_eq_degree_of_separable_witness
  - HasseWeil.card_kernel_eq_degree_of_separable_coordHom
- «matrix-det-quadratic»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.det_smul_sub_smul_one_fin_two
  - HasseWeil.WeilPairing.det_one_sub_fin_two
- «mul-by-n-degree»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.mulByInt
  - HasseWeil.mulByInt_degree
- «mul-by-n-trace»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HasseWeil.isogTrace_mulByInt
- «one-sub-frobenius-separable»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.oneSubFrobenius_isSeparable_of_witness
  - HasseWeil.isSeparable_iff_of_coeff_witness
- «point-count»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HasseWeil.pointCount
- «pointcount-eq-trace»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.pointCount_eq_of_witness
  - HasseWeil.pointCount_eq_of_hom_kernel_witness
- «qf-coprime-to-all»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime_both
- «qf-nonneg-weil»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data_both
- «sqrt-bound»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HasseWeil.abs_le_two_sqrt_of_sq_le
- «sum-trace-frobenius»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HasseWeil.sum_trace_frobenius_witness
  - HasseWeil.dual_comp_frobenius_witness
- «trace-sq-le-four-q»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HasseWeil.trace_sq_le_four_mul_deg

Untagged (30)

isogeny(Definition)

Missing tag metadata.
Associated lean decls (2)
- HasseWeil.Isogeny
- HasseWeil.Isogeny.degree
«deg-one-sub-pi-eq-pointcount»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- HasseWeil.isogOneSub_negFrobenius_degree_eq_pointCount
- HasseWeil.kernel_eq_top_of_hom_eq_id_sub_frobenius
«degree-multiplicative»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- HasseWeil.Isogeny.comp_degree
- HasseWeil.Isogeny.comp_degree_pos
«degree-nonneg»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- HasseWeil.qf_nonneg_of_genuine_chain
- HasseWeil.degree_quadratic_mulByInt_nonneg
«degree-quadratic-form»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- HasseWeil.traceOfFrobenius_sq_le_of_qf_nonneg
«degree-quadratic-polarisation»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- HasseWeil.degree_quadratic_genuine_addIsog
«degree-quadratic-scalar»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- HasseWeil.degree_quadratic_mulByInt
«det-deg»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- HasseWeil.WeilPairing.TorsionGeometric.det_rhoEll_eq_degree
- HasseWeil.WeilPairing.TorsionGeometric.linearMap_det_torsionRestrict_eq
«dual-additivity»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- HasseWeil.dual_add_of_trace_witnesses
- HasseWeil.dual_add_of_sum_witnesses
«dual-isogeny»(Definition)

Missing tag metadata.
Associated lean decls (2)
- HasseWeil.IsDualOf
- HasseWeil.degree_dual_of_witness
Show all 20 more untagged entries
- «frob-det-data»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.TorsionGeometric.frob_det_residual_of_weil_scaling
  - HasseWeil.WeilPairing.frob_det_residual_baseChange
- «frobenius-degree»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.frobeniusIsog_degree
  - HasseWeil.frobenius_finrank_functionField
- «frobenius-fixed-locus»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.frobenius_fixed_iff_mem_baseField
  - HasseWeil.range_algebraMap_eq_roots_X_pow_card_sub_X
- «frobenius-isogeny»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.frobeniusIsog
  - HasseWeil.frobeniusIsog_pullback_apply
- «hasse-bound-from-witnesses»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.hasse_bound_of_qf_nonneg_witnesses
  - HasseWeil.hasse_bound_of_full_qf_nonneg_witnesses
- «hasse-bound-weil-capstone»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.hasse_bound_via_weil_pairing
  - HasseWeil.WeilPairing.hasse_bound_unconditional_of_baseChange_scalings_coprime
- «hasse-bound»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.hasse_bound
  - HasseWeil.WeilPairing.hasse_bound_unconditional
- «isog-trace»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HasseWeil.isogTrace
- «kernel-card-degree»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.Isogeny.card_kernel_eq_degree_of_separable_witness
  - HasseWeil.card_kernel_eq_degree_of_separable_coordHom
- «matrix-det-quadratic»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.det_smul_sub_smul_one_fin_two
  - HasseWeil.WeilPairing.det_one_sub_fin_two
- «mul-by-n-degree»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.mulByInt
  - HasseWeil.mulByInt_degree
- «mul-by-n-trace»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HasseWeil.isogTrace_mulByInt
- «one-sub-frobenius-separable»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.oneSubFrobenius_isSeparable_of_witness
  - HasseWeil.isSeparable_iff_of_coeff_witness
- «point-count»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HasseWeil.pointCount
- «pointcount-eq-trace»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.pointCount_eq_of_witness
  - HasseWeil.pointCount_eq_of_hom_kernel_witness
- «qf-coprime-to-all»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime_both
- «qf-nonneg-weil»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data_both
- «sqrt-bound»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HasseWeil.abs_le_two_sqrt_of_sq_le
- «sum-trace-frobenius»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HasseWeil.sum_trace_frobenius_witness
  - HasseWeil.dual_comp_frobenius_witness
- «trace-sq-le-four-q»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HasseWeil.trace_sq_le_four_mul_deg

Structure and coverage

Fully closed30Local code and ancestor closure are both complete.

Heaviest prerequisites (23)

«hasse-bound-weil-capstone»(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 (2)
- HasseWeil.WeilPairing.hasse_bound_via_weil_pairing
- HasseWeil.WeilPairing.hasse_bound_unconditional_of_baseChange_scalings_coprime
«hasse-bound»(Theorem)

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

total deps: 4statement deps: 0proof deps: 4direct uses: 1downstream unlocks: 1
Associated lean decls (2)
- HasseWeil.WeilPairing.hasse_bound
- HasseWeil.WeilPairing.hasse_bound_unconditional
«hasse-bound-from-witnesses»(Theorem)

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

total deps: 4statement deps: 2proof deps: 3direct uses: 1downstream unlocks: 1
Associated lean decls (2)
- HasseWeil.hasse_bound_of_qf_nonneg_witnesses
- HasseWeil.hasse_bound_of_full_qf_nonneg_witnesses
«degree-quadratic-polarisation»(Theorem)

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

total deps: 3statement deps: 0proof deps: 3direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- HasseWeil.degree_quadratic_genuine_addIsog
«frob-det-data»(Theorem)

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

total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 2
Associated lean decls (2)
- HasseWeil.WeilPairing.TorsionGeometric.frob_det_residual_of_weil_scaling
- HasseWeil.WeilPairing.frob_det_residual_baseChange
«pointcount-eq-trace»(Theorem)

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

total deps: 3statement deps: 0proof deps: 3direct uses: 3downstream unlocks: 2
Associated lean decls (2)
- HasseWeil.pointCount_eq_of_witness
- HasseWeil.pointCount_eq_of_hom_kernel_witness
«sum-trace-frobenius»(Theorem)

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

total deps: 3statement deps: 0proof deps: 3direct uses: 1downstream unlocks: 4
Associated lean decls (2)
- HasseWeil.sum_trace_frobenius_witness
- HasseWeil.dual_comp_frobenius_witness
«deg-one-sub-pi-eq-pointcount»(Theorem)

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

total deps: 3statement deps: 1proof deps: 2direct uses: 1downstream unlocks: 3
Associated lean decls (2)
- HasseWeil.isogOneSub_negFrobenius_degree_eq_pointCount
- HasseWeil.kernel_eq_top_of_hom_eq_id_sub_frobenius
«degree-quadratic-scalar»(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)
- HasseWeil.degree_quadratic_mulByInt
«mul-by-n-degree»(Theorem)

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

total deps: 2statement deps: 0proof deps: 2direct uses: 3downstream unlocks: 10
Associated lean decls (2)
- HasseWeil.mulByInt
- HasseWeil.mulByInt_degree
Show all 13 more heaviest-prerequisite entries
- «qf-nonneg-weil»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 0proof deps: 2direct uses: 1downstream unlocks: 1
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data
  - HasseWeil.WeilPairing.qf_nonneg_skeleton_of_weil_det_data_both
- «degree-quadratic-form»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 2
  Associated lean decls (1)
  - HasseWeil.traceOfFrobenius_sq_le_of_qf_nonneg
- «dual-isogeny»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 6
  Associated lean decls (2)
  - HasseWeil.IsDualOf
  - HasseWeil.degree_dual_of_witness
- «mul-by-n-trace»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 2downstream unlocks: 10
  Associated lean decls (1)
  - HasseWeil.isogTrace_mulByInt
- «degree-nonneg»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 1direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - HasseWeil.qf_nonneg_of_genuine_chain
  - HasseWeil.degree_quadratic_mulByInt_nonneg
- «one-sub-frobenius-separable»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 4
  Associated lean decls (2)
  - HasseWeil.oneSubFrobenius_isSeparable_of_witness
  - HasseWeil.isSeparable_iff_of_coeff_witness
- «qf-coprime-to-all»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime
  - HasseWeil.WeilPairing.qf_nonneg_of_nonneg_on_coprime_both
- «sqrt-bound»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 0proof deps: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - HasseWeil.abs_le_two_sqrt_of_sq_le
- «degree-multiplicative»(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 (2)
  - HasseWeil.Isogeny.comp_degree
  - HasseWeil.Isogeny.comp_degree_pos
- «dual-additivity»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 5
  Associated lean decls (2)
  - HasseWeil.dual_add_of_trace_witnesses
  - HasseWeil.dual_add_of_sum_witnesses
- «frobenius-degree»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 8
  Associated lean decls (2)
  - HasseWeil.frobeniusIsog_degree
  - HasseWeil.frobenius_finrank_functionField
- «frobenius-isogeny»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 5downstream unlocks: 19
  Associated lean decls (2)
  - HasseWeil.frobeniusIsog
  - HasseWeil.frobeniusIsog_pullback_apply
- «isog-trace»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 11
  Associated lean decls (1)
  - HasseWeil.isogTrace

No prerequisites (7)

isogeny(Definition)
Associated lean decls (2)
- HasseWeil.Isogeny
- HasseWeil.Isogeny.degree
«kernel-card-degree»(Theorem)
Associated lean decls (2)
- HasseWeil.Isogeny.card_kernel_eq_degree_of_separable_witness
- HasseWeil.card_kernel_eq_degree_of_separable_coordHom
«point-count»(Definition)
Associated lean decls (1)
- HasseWeil.pointCount
«det-deg»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.TorsionGeometric.det_rhoEll_eq_degree
- HasseWeil.WeilPairing.TorsionGeometric.linearMap_det_torsionRestrict_eq
«matrix-det-quadratic»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.det_smul_sub_smul_one_fin_two
- HasseWeil.WeilPairing.det_one_sub_fin_two
«frobenius-fixed-locus»(Theorem)
Associated lean decls (2)
- HasseWeil.frobenius_fixed_iff_mem_baseField
- HasseWeil.range_algebraMap_eq_roots_X_pow_card_sub_X
«trace-sq-le-four-q»(Theorem)
Associated lean decls (1)
- HasseWeil.trace_sq_le_four_mul_deg

No dependents (3)

«hasse-bound-weil-capstone»(Theorem)
Associated lean decls (2)
- HasseWeil.WeilPairing.hasse_bound_via_weil_pairing
- HasseWeil.WeilPairing.hasse_bound_unconditional_of_baseChange_scalings_coprime
«degree-multiplicative»(Theorem)
Associated lean decls (2)
- HasseWeil.Isogeny.comp_degree
- HasseWeil.Isogeny.comp_degree_pos
«degree-quadratic-scalar»(Theorem)
Associated lean decls (1)
- HasseWeil.degree_quadratic_mulByInt