Blueprint Summary🔗

Overview

Total entries28completed: 28; deps incomplete: 0; sorries: 0; no proof: 0

Ready now0Entries whose next formalization step is currently unblocked.

Fully closed28Local code and prerequisite closure are both complete.

Actionable priorities0Entries ready now and already unlocking downstream work.

Entry index (28)

Definitions9completed: 9; deps incomplete: 0; sorries: 0; no proof: 0

Theorems19completed: 19; deps incomplete: 0; sorries: 0; no proof: 0

Definition Index (9)

«hecke-operator-tn»(Definition)
Associated lean decls (2)
- HeckeRing.GL2.heckeT_n
- HeckeRing.GL2.heckeT_n_cusp
«level-raise»(Definition)
Associated lean decls (2)
- HeckeRing.GL2.levelRaise
- HeckeRing.GL2.levelInclude_cusp
«hecke-character-space»(Definition)
Associated lean decls (1)
- HeckeRing.GL2.modFormCharSpace
«cusp-forms-new-old»(Definition)
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld
- HeckeRing.GL2.cuspFormsNew
eigenform(Definition)
Associated lean decls (2)
- HeckeRing.GL2.Eigenform
- HeckeRing.GL2.Eigenform.eigenvalue
«old-new-part»(Definition)
Associated lean decls (2)
- HeckeRing.GL2.oldPart
- HeckeRing.GL2.newPart
petersson(Definition)
Associated lean decls (2)
- HeckeRing.GL2.petN_self_re_nonneg
- HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues
«diamond-operator»(Definition)
Associated lean decls (1)
- HeckeRing.GL2.diamondOpHom
newform(Definition)
Associated lean decls (1)
- HeckeRing.GL2.Newform

Theorem / Proposition / Lemma / Corollary Index (19)

«smo-const-mul»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.strongMultiplicityOne_constMul
«old-part-hecke-comm»(Theorem)
Associated lean decls (2)
- HeckeRing.GL2.oldPart_heckeT_n_cusp_comm
- HeckeRing.GL2.oldPart_isEigen_of_eigenform
«coeff-action»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.fourierCoeff_heckeT_n_period_one
«new-part-eq-smul»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.newPart_eq_smul_of_shared_eigenvalues
«level-raise-eigen»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.heckeT_n_levelRaise_eigen
«newform-not-old»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.newform_notMem_cuspFormsOldExtended
«old-part-vanishing»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.oldPart_eq_zero_of_shared_eigenvalues
«char-space-decomp»(Theorem)
Associated lean decls (2)
- HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace
- HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace
«strong-multiplicity-one»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.strongMultiplicityOne_axiom_clean
«coeff-eigenvalue»(Theorem)
Associated lean decls (2)
- HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue
- HeckeRing.GL2.Newform.eigenvalue_eq_coeff
«hecke-commute-diamond»(Theorem)
Associated lean decls (2)
- HeckeRing.GL2.heckeT_n_comm_diamondOp
- HeckeRing.GL2.heckeT_n_preserves_charSpace
«main-lemma»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.mainLemma_charSpace_routeB
«old-space-eigen-normal-form»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
«hecke-commute»(Theorem)
Associated lean decls (2)
- HeckeRing.GL2.heckeT_n_comm
- HeckeRing.GL2.heckeT_n_mul_coprime
«old-space-isotypic-identification»(Theorem)
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld_inf_charSpace_le_cuspFormsOldChar
- HeckeRing.GL2.cuspFormsOldChar_le_cuspFormsOld
«coeff-one-ne-zero»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen
«old-new-disjoint»(Theorem)
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld_disjoint_cuspFormsNew
- HeckeRing.GL2.cuspFormsOld_isCompl_cuspFormsNew
«eigenform-decomp»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew
«eigenvalue-multiplicative»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.eigenform_coeff_multiplicative_one

Dependency insights

Statement-used entries19Entries reused in statement dependencies.

Proof-used entries19Entries reused in proof-only dependencies.

Most used in statements (19)

«cusp-forms-new-old»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 9proof uses: 0direct uses: 9downstream unlocks: 14
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld
- HeckeRing.GL2.cuspFormsNew
eigenform(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 7proof uses: 0direct uses: 7downstream unlocks: 19
Associated lean decls (2)
- HeckeRing.GL2.Eigenform
- HeckeRing.GL2.Eigenform.eigenvalue
newform(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 5proof uses: 0direct uses: 5downstream unlocks: 5
Associated lean decls (1)
- HeckeRing.GL2.Newform
«hecke-operator-tn»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 23
Associated lean decls (2)
- HeckeRing.GL2.heckeT_n
- HeckeRing.GL2.heckeT_n_cusp
«hecke-character-space»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 4proof uses: 0direct uses: 4downstream unlocks: 22
Associated lean decls (1)
- HeckeRing.GL2.modFormCharSpace
«level-raise»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 3proof uses: 0direct uses: 3downstream unlocks: 16
Associated lean decls (2)
- HeckeRing.GL2.levelRaise
- HeckeRing.GL2.levelInclude_cusp
«diamond-operator»(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 0direct uses: 2downstream unlocks: 24
Associated lean decls (1)
- HeckeRing.GL2.diamondOpHom
petersson(Definition)

Reverse dependencies recorded in statement dependencies.

statement uses: 2proof uses: 1direct uses: 3downstream unlocks: 15
Associated lean decls (2)
- HeckeRing.GL2.petN_self_re_nonneg
- HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues
«hecke-commute-diamond»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 6
Associated lean decls (2)
- HeckeRing.GL2.heckeT_n_comm_diamondOp
- HeckeRing.GL2.heckeT_n_preserves_charSpace
«coeff-eigenvalue»(Theorem)

Reverse dependencies recorded in statement dependencies.

statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 5
Associated lean decls (2)
- HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue
- HeckeRing.GL2.Newform.eigenvalue_eq_coeff
Show all 9 more statement-used entries
- «coeff-one-ne-zero»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 2direct uses: 3downstream unlocks: 4
  Associated lean decls (1)
  - HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen
- «eigenform-decomp»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 4
  Associated lean decls (1)
  - HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew
- «char-space-decomp»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (2)
  - HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace
  - HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace
- «newform-not-old»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - HeckeRing.GL2.newform_notMem_cuspFormsOldExtended
- «old-new-part»(Definition)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart
  - HeckeRing.GL2.newPart
- «old-space-eigen-normal-form»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
- «new-part-eq-smul»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - HeckeRing.GL2.newPart_eq_smul_of_shared_eigenvalues
- «old-part-vanishing»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - HeckeRing.GL2.oldPart_eq_zero_of_shared_eigenvalues
- «smo-const-mul»(Theorem)
  
  Reverse dependencies recorded in statement dependencies.
  
  statement uses: 1proof uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - HeckeRing.GL2.strongMultiplicityOne_constMul

Most used in proofs (19)

«main-lemma»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 3statement uses: 0direct uses: 3downstream unlocks: 5
Associated lean decls (1)
- HeckeRing.GL2.mainLemma_charSpace_routeB
«coeff-action»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 7
Associated lean decls (1)
- HeckeRing.GL2.fourierCoeff_heckeT_n_period_one
«hecke-commute»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 7
Associated lean decls (2)
- HeckeRing.GL2.heckeT_n_comm
- HeckeRing.GL2.heckeT_n_mul_coprime
«old-new-disjoint»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 0direct uses: 2downstream unlocks: 6
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld_disjoint_cuspFormsNew
- HeckeRing.GL2.cuspFormsOld_isCompl_cuspFormsNew
«coeff-eigenvalue»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 5
Associated lean decls (2)
- HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue
- HeckeRing.GL2.Newform.eigenvalue_eq_coeff
«coeff-one-ne-zero»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 2statement uses: 1direct uses: 3downstream unlocks: 4
Associated lean decls (1)
- HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen
petersson(Definition)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 2direct uses: 3downstream unlocks: 15
Associated lean decls (2)
- HeckeRing.GL2.petN_self_re_nonneg
- HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues
«hecke-commute-diamond»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 6
Associated lean decls (2)
- HeckeRing.GL2.heckeT_n_comm_diamondOp
- HeckeRing.GL2.heckeT_n_preserves_charSpace
«eigenform-decomp»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 4
Associated lean decls (1)
- HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew
«char-space-decomp»(Theorem)

Reverse dependencies recorded in proof dependencies.

proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
Associated lean decls (2)
- HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace
- HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace
Show all 9 more proof-used entries
- «newform-not-old»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - HeckeRing.GL2.newform_notMem_cuspFormsOldExtended
- «old-new-part»(Definition)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart
  - HeckeRing.GL2.newPart
- «old-space-eigen-normal-form»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 3
  Associated lean decls (1)
  - HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
- «eigenvalue-multiplicative»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 3
  Associated lean decls (1)
  - HeckeRing.GL2.eigenform_coeff_multiplicative_one
- «new-part-eq-smul»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - HeckeRing.GL2.newPart_eq_smul_of_shared_eigenvalues
- «old-part-vanishing»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 2
  Associated lean decls (1)
  - HeckeRing.GL2.oldPart_eq_zero_of_shared_eigenvalues
- «old-part-hecke-comm»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart_heckeT_n_cusp_comm
  - HeckeRing.GL2.oldPart_isEigen_of_eigenform
- «old-space-isotypic-identification»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 0direct uses: 1downstream unlocks: 2
  Associated lean decls (2)
  - HeckeRing.GL2.cuspFormsOld_inf_charSpace_le_cuspFormsOldChar
  - HeckeRing.GL2.cuspFormsOldChar_le_cuspFormsOld
- «smo-const-mul»(Theorem)
  
  Reverse dependencies recorded in proof dependencies.
  
  proof uses: 1statement uses: 1direct uses: 2downstream unlocks: 1
  Associated lean decls (1)
  - HeckeRing.GL2.strongMultiplicityOne_constMul

Metadata

Metadata audit

Missing owner28

Missing effort28

Untagged28

Missing owner (28)

eigenform(Definition)

Missing owner metadata.
Associated lean decls (2)
- HeckeRing.GL2.Eigenform
- HeckeRing.GL2.Eigenform.eigenvalue
newform(Definition)

Missing owner metadata.
Associated lean decls (1)
- HeckeRing.GL2.Newform
petersson(Definition)

Missing owner metadata.
Associated lean decls (2)
- HeckeRing.GL2.petN_self_re_nonneg
- HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues
«char-space-decomp»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace
- HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace
«coeff-action»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- HeckeRing.GL2.fourierCoeff_heckeT_n_period_one
«coeff-eigenvalue»(Theorem)

Missing owner metadata.
Associated lean decls (2)
- HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue
- HeckeRing.GL2.Newform.eigenvalue_eq_coeff
«coeff-one-ne-zero»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen
«cusp-forms-new-old»(Definition)

Missing owner metadata.
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld
- HeckeRing.GL2.cuspFormsNew
«diamond-operator»(Definition)

Missing owner metadata.
Associated lean decls (1)
- HeckeRing.GL2.diamondOpHom
«eigenform-decomp»(Theorem)

Missing owner metadata.
Associated lean decls (1)
- HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew
Show all 18 more entries missing owner
- «eigenvalue-multiplicative»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.eigenform_coeff_multiplicative_one
- «hecke-character-space»(Definition)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.modFormCharSpace
- «hecke-commute-diamond»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n_comm_diamondOp
  - HeckeRing.GL2.heckeT_n_preserves_charSpace
- «hecke-commute»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n_comm
  - HeckeRing.GL2.heckeT_n_mul_coprime
- «hecke-operator-tn»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n
  - HeckeRing.GL2.heckeT_n_cusp
- «level-raise-eigen»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.heckeT_n_levelRaise_eigen
- «level-raise»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.levelRaise
  - HeckeRing.GL2.levelInclude_cusp
- «main-lemma»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.mainLemma_charSpace_routeB
- «new-part-eq-smul»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.newPart_eq_smul_of_shared_eigenvalues
- «newform-not-old»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.newform_notMem_cuspFormsOldExtended
- «old-new-disjoint»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.cuspFormsOld_disjoint_cuspFormsNew
  - HeckeRing.GL2.cuspFormsOld_isCompl_cuspFormsNew
- «old-new-part»(Definition)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart
  - HeckeRing.GL2.newPart
- «old-part-hecke-comm»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart_heckeT_n_cusp_comm
  - HeckeRing.GL2.oldPart_isEigen_of_eigenform
- «old-part-vanishing»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.oldPart_eq_zero_of_shared_eigenvalues
- «old-space-eigen-normal-form»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
- «old-space-isotypic-identification»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.cuspFormsOld_inf_charSpace_le_cuspFormsOldChar
  - HeckeRing.GL2.cuspFormsOldChar_le_cuspFormsOld
- «smo-const-mul»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.strongMultiplicityOne_constMul
- «strong-multiplicity-one»(Theorem)
  
  Missing owner metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.strongMultiplicityOne_axiom_clean

Missing effort (28)

eigenform(Definition)

Missing effort metadata.
Associated lean decls (2)
- HeckeRing.GL2.Eigenform
- HeckeRing.GL2.Eigenform.eigenvalue
newform(Definition)

Missing effort metadata.
Associated lean decls (1)
- HeckeRing.GL2.Newform
petersson(Definition)

Missing effort metadata.
Associated lean decls (2)
- HeckeRing.GL2.petN_self_re_nonneg
- HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues
«char-space-decomp»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace
- HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace
«coeff-action»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- HeckeRing.GL2.fourierCoeff_heckeT_n_period_one
«coeff-eigenvalue»(Theorem)

Missing effort metadata.
Associated lean decls (2)
- HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue
- HeckeRing.GL2.Newform.eigenvalue_eq_coeff
«coeff-one-ne-zero»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen
«cusp-forms-new-old»(Definition)

Missing effort metadata.
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld
- HeckeRing.GL2.cuspFormsNew
«diamond-operator»(Definition)

Missing effort metadata.
Associated lean decls (1)
- HeckeRing.GL2.diamondOpHom
«eigenform-decomp»(Theorem)

Missing effort metadata.
Associated lean decls (1)
- HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew
Show all 18 more entries missing effort
- «eigenvalue-multiplicative»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.eigenform_coeff_multiplicative_one
- «hecke-character-space»(Definition)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.modFormCharSpace
- «hecke-commute-diamond»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n_comm_diamondOp
  - HeckeRing.GL2.heckeT_n_preserves_charSpace
- «hecke-commute»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n_comm
  - HeckeRing.GL2.heckeT_n_mul_coprime
- «hecke-operator-tn»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n
  - HeckeRing.GL2.heckeT_n_cusp
- «level-raise-eigen»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.heckeT_n_levelRaise_eigen
- «level-raise»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.levelRaise
  - HeckeRing.GL2.levelInclude_cusp
- «main-lemma»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.mainLemma_charSpace_routeB
- «new-part-eq-smul»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.newPart_eq_smul_of_shared_eigenvalues
- «newform-not-old»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.newform_notMem_cuspFormsOldExtended
- «old-new-disjoint»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.cuspFormsOld_disjoint_cuspFormsNew
  - HeckeRing.GL2.cuspFormsOld_isCompl_cuspFormsNew
- «old-new-part»(Definition)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart
  - HeckeRing.GL2.newPart
- «old-part-hecke-comm»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart_heckeT_n_cusp_comm
  - HeckeRing.GL2.oldPart_isEigen_of_eigenform
- «old-part-vanishing»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.oldPart_eq_zero_of_shared_eigenvalues
- «old-space-eigen-normal-form»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
- «old-space-isotypic-identification»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.cuspFormsOld_inf_charSpace_le_cuspFormsOldChar
  - HeckeRing.GL2.cuspFormsOldChar_le_cuspFormsOld
- «smo-const-mul»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.strongMultiplicityOne_constMul
- «strong-multiplicity-one»(Theorem)
  
  Missing effort metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.strongMultiplicityOne_axiom_clean

Untagged (28)

eigenform(Definition)

Missing tag metadata.
Associated lean decls (2)
- HeckeRing.GL2.Eigenform
- HeckeRing.GL2.Eigenform.eigenvalue
newform(Definition)

Missing tag metadata.
Associated lean decls (1)
- HeckeRing.GL2.Newform
petersson(Definition)

Missing tag metadata.
Associated lean decls (2)
- HeckeRing.GL2.petN_self_re_nonneg
- HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues
«char-space-decomp»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace
- HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace
«coeff-action»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- HeckeRing.GL2.fourierCoeff_heckeT_n_period_one
«coeff-eigenvalue»(Theorem)

Missing tag metadata.
Associated lean decls (2)
- HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue
- HeckeRing.GL2.Newform.eigenvalue_eq_coeff
«coeff-one-ne-zero»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen
«cusp-forms-new-old»(Definition)

Missing tag metadata.
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld
- HeckeRing.GL2.cuspFormsNew
«diamond-operator»(Definition)

Missing tag metadata.
Associated lean decls (1)
- HeckeRing.GL2.diamondOpHom
«eigenform-decomp»(Theorem)

Missing tag metadata.
Associated lean decls (1)
- HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew
Show all 18 more untagged entries
- «eigenvalue-multiplicative»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.eigenform_coeff_multiplicative_one
- «hecke-character-space»(Definition)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.modFormCharSpace
- «hecke-commute-diamond»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n_comm_diamondOp
  - HeckeRing.GL2.heckeT_n_preserves_charSpace
- «hecke-commute»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n_comm
  - HeckeRing.GL2.heckeT_n_mul_coprime
- «hecke-operator-tn»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.heckeT_n
  - HeckeRing.GL2.heckeT_n_cusp
- «level-raise-eigen»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.heckeT_n_levelRaise_eigen
- «level-raise»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.levelRaise
  - HeckeRing.GL2.levelInclude_cusp
- «main-lemma»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.mainLemma_charSpace_routeB
- «new-part-eq-smul»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.newPart_eq_smul_of_shared_eigenvalues
- «newform-not-old»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.newform_notMem_cuspFormsOldExtended
- «old-new-disjoint»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.cuspFormsOld_disjoint_cuspFormsNew
  - HeckeRing.GL2.cuspFormsOld_isCompl_cuspFormsNew
- «old-new-part»(Definition)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart
  - HeckeRing.GL2.newPart
- «old-part-hecke-comm»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart_heckeT_n_cusp_comm
  - HeckeRing.GL2.oldPart_isEigen_of_eigenform
- «old-part-vanishing»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.oldPart_eq_zero_of_shared_eigenvalues
- «old-space-eigen-normal-form»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
- «old-space-isotypic-identification»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (2)
  - HeckeRing.GL2.cuspFormsOld_inf_charSpace_le_cuspFormsOldChar
  - HeckeRing.GL2.cuspFormsOldChar_le_cuspFormsOld
- «smo-const-mul»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.strongMultiplicityOne_constMul
- «strong-multiplicity-one»(Theorem)
  
  Missing tag metadata.
  Associated lean decls (1)
  - HeckeRing.GL2.strongMultiplicityOne_axiom_clean

Structure and coverage

Fully closed28Local code and ancestor closure are both complete.

Heaviest prerequisites (25)

«old-part-vanishing»(Theorem)

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

total deps: 6statement deps: 3proof deps: 5direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- HeckeRing.GL2.oldPart_eq_zero_of_shared_eigenvalues
«smo-const-mul»(Theorem)

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

total deps: 6statement deps: 3proof deps: 5direct uses: 2downstream unlocks: 1
Associated lean decls (1)
- HeckeRing.GL2.strongMultiplicityOne_constMul
«new-part-eq-smul»(Theorem)

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

total deps: 5statement deps: 3proof deps: 4direct uses: 2downstream unlocks: 2
Associated lean decls (1)
- HeckeRing.GL2.newPart_eq_smul_of_shared_eigenvalues
«coeff-one-ne-zero»(Theorem)

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

total deps: 5statement deps: 2proof deps: 3direct uses: 3downstream unlocks: 4
Associated lean decls (1)
- HeckeRing.GL2.coeff_one_ne_zero_of_mem_cuspFormsNew_of_eigen
«eigenform-decomp»(Theorem)

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

total deps: 4statement deps: 2proof deps: 2direct uses: 2downstream unlocks: 4
Associated lean decls (1)
- HeckeRing.GL2.exists_eigenform_decomposition_mem_cuspFormsNew
«eigenvalue-multiplicative»(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 (1)
- HeckeRing.GL2.eigenform_coeff_multiplicative_one
«old-space-eigen-normal-form»(Theorem)

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

total deps: 3statement deps: 3proof deps: 1direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- HeckeRing.GL2.exists_levelRaise_eigen_decomposition_of_mem_cuspFormsOldChar
«newform-not-old»(Theorem)

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

total deps: 3statement deps: 2proof deps: 1direct uses: 2downstream unlocks: 3
Associated lean decls (1)
- HeckeRing.GL2.newform_notMem_cuspFormsOldExtended
«old-space-isotypic-identification»(Theorem)

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

total deps: 2statement deps: 2proof deps: 1direct uses: 1downstream unlocks: 2
Associated lean decls (2)
- HeckeRing.GL2.cuspFormsOld_inf_charSpace_le_cuspFormsOldChar
- HeckeRing.GL2.cuspFormsOldChar_le_cuspFormsOld
«strong-multiplicity-one»(Theorem)

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

total deps: 2statement deps: 2proof deps: 1direct uses: 0downstream unlocks: 0
Associated lean decls (1)
- HeckeRing.GL2.strongMultiplicityOne_axiom_clean
Show all 15 more heaviest-prerequisite entries
- «coeff-eigenvalue»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 1proof deps: 1direct uses: 3downstream unlocks: 5
  Associated lean decls (2)
  - HeckeRing.GL2.Eigenform.coeff_eq_coeff_one_mul_eigenvalue
  - HeckeRing.GL2.Newform.eigenvalue_eq_coeff
- eigenform(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 7downstream unlocks: 19
  Associated lean decls (2)
  - HeckeRing.GL2.Eigenform
  - HeckeRing.GL2.Eigenform.eigenvalue
- newform(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 5downstream unlocks: 5
  Associated lean decls (1)
  - HeckeRing.GL2.Newform
- «coeff-action»(Theorem)
  
  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)
  - HeckeRing.GL2.fourierCoeff_heckeT_n_period_one
- «cusp-forms-new-old»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 9downstream unlocks: 14
  Associated lean decls (2)
  - HeckeRing.GL2.cuspFormsOld
  - HeckeRing.GL2.cuspFormsNew
- «hecke-commute-diamond»(Theorem)
  
  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)
  - HeckeRing.GL2.heckeT_n_comm_diamondOp
  - HeckeRing.GL2.heckeT_n_preserves_charSpace
- «level-raise-eigen»(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)
  - HeckeRing.GL2.heckeT_n_levelRaise_eigen
- «main-lemma»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 2statement deps: 2proof deps: 0direct uses: 3downstream unlocks: 5
  Associated lean decls (1)
  - HeckeRing.GL2.mainLemma_charSpace_routeB
- «old-new-disjoint»(Theorem)
  
  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)
  - HeckeRing.GL2.cuspFormsOld_disjoint_cuspFormsNew
  - HeckeRing.GL2.cuspFormsOld_isCompl_cuspFormsNew
- «old-part-hecke-comm»(Theorem)
  
  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 (2)
  - HeckeRing.GL2.oldPart_heckeT_n_cusp_comm
  - HeckeRing.GL2.oldPart_isEigen_of_eigenform
- petersson(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 3downstream unlocks: 15
  Associated lean decls (2)
  - HeckeRing.GL2.petN_self_re_nonneg
  - HeckeRing.GL2.eigenforms_orthogonal_of_ne_eigenvalues
- «char-space-decomp»(Theorem)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (2)
  - HeckeRing.GL2.ModularForm_Gamma1_iSup_charSpace
  - HeckeRing.GL2.ModularForm_Gamma1_iSupIndep_charSpace
- «hecke-character-space»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 4downstream unlocks: 22
  Associated lean decls (1)
  - HeckeRing.GL2.modFormCharSpace
- «hecke-commute»(Theorem)
  
  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 (2)
  - HeckeRing.GL2.heckeT_n_comm
  - HeckeRing.GL2.heckeT_n_mul_coprime
- «old-new-part»(Definition)
  
  Prerequisite fan-in measured from the current statement/proof dependency graph.
  
  total deps: 1statement deps: 1proof deps: 0direct uses: 2downstream unlocks: 3
  Associated lean decls (2)
  - HeckeRing.GL2.oldPart
  - HeckeRing.GL2.newPart

No prerequisites (3)

«hecke-operator-tn»(Definition)
Associated lean decls (2)
- HeckeRing.GL2.heckeT_n
- HeckeRing.GL2.heckeT_n_cusp
«diamond-operator»(Definition)
Associated lean decls (1)
- HeckeRing.GL2.diamondOpHom
«level-raise»(Definition)
Associated lean decls (2)
- HeckeRing.GL2.levelRaise
- HeckeRing.GL2.levelInclude_cusp

No dependents (2)

«strong-multiplicity-one»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.strongMultiplicityOne_axiom_clean
«level-raise-eigen»(Theorem)
Associated lean decls (1)
- HeckeRing.GL2.heckeT_n_levelRaise_eigen