Namespace HeckeEis 130 theorems
— 119 · IsEichlerIntegral 10 · IsEquivariantPrimitiveWith 1
directly in HeckeEis 119
- Hecke conjugation commutes with diag(ℓ,1) on binary forms
HeckeEis.binaryFormAlphaAdj_comp_binaryFormRepSL_heckeConj0 below · cited by 15 · depth 11 - Coefficient change is Hecke-equivariant on parabolic H¹
HeckeEis.coeffH1par_map_heckeT_comm0 below · cited by 5 · depth 11 - Integral basis of parabolic cohomology maps to a complex basis
HeckeEis.exists_basis_coeffH1par_int_complex10 below · cited by 5 · depth 11 - Existence of the induced Hecke endomorphism of H¹ₚₐᵣ
HeckeEis.exists_coeffH1par_linearMap_coeffHeckeFun4 below · cited by 4 · depth 11 - Change of coefficients for parabolic H¹ of binary forms
HeckeEis.exists_coeffH1par_map_ringHom0 below · cited by 6 · depth 11 - Hecke-equivariant Eichler–Shimura decomposition of parabolic cohomology
HeckeEis.exists_eichlerShimura_coeffH1par_binaryFormRepSL_forall_prime644 below · cited by 2 · depth 11 - Image of integral parabolic cohomology spans the complex one
HeckeEis.span_range_coeffH1par_map_int_complex_eq_top11 below · cited by 1 · depth 11 - Evaluation map intertwines diag(ℓ,1) on forms and on P¹(ℤ/p)
HeckeEis.binaryFormEval_binaryFormAlphaAdj0 below · cited by 2 · depth 12 - SL₂(ℤ)-equivariance of evaluation of binary forms on P¹(ℤ/p)
HeckeEis.binaryFormEval_binaryFormRepSL0 below · cited by 2 · depth 12 - Torsion-freeness of integral parabolic H¹ for Γ₀(N)
HeckeEis.coeffH1par_binaryFormRepSL_int_eq_zero_of_smul_eq_zero2 below · cited by 3 · depth 12 - Injectivity of H¹ₚₐᵣ from ℤ to ℚ
HeckeEis.coeffH1par_map_int_rat_injective3 below · cited by 1 · depth 12 - Cochain Hecke operator preserves coefficient coboundaries
HeckeEis.coeffHeckeFun_mem_coeffCoboundaries0 below · cited by 23 · depth 12 - Cochain-level Hecke operator preserves 1-cocycles
HeckeEis.coeffHeckeFun_mem_coeffCocycles0 below · cited by 24 · depth 12 - Hecke operator preserves parabolic cocycles with coefficients
HeckeEis.coeffHeckeFun_mem_coeffParabolicCocycles2 below · cited by 3 · depth 12 - Coset-sum corestriction equals the transfer homomorphism
HeckeEis.coresHom_eq_transfer0 below · cited by 6 · depth 12 - Corestriction after restriction is multiplication by the index
HeckeEis.coresHom_resHom_apply0 below · cited by 2 · depth 12 - Hecke equivariance of the twisted degeneracy transfer
HeckeEis.degeneracyTransferZero_heckeOperatorHom_comm0 below · cited by 1 · depth 12 - Eichler–Shimura map intertwines T_ℓ with cohomological T_ℓ
HeckeEis.eichlerShimuraMap_heckeTLin17 below · cited by 3 · depth 12 - Eichler–Shimura map intertwines U_ℓ for ℓ ∣ N
HeckeEis.eichlerShimuraMap_heckeULin17 below · cited by 1 · depth 12 - Injectivity of the Eichler–Shimura map on cusp forms
HeckeEis.eichlerShimuraMap_injective26 below · cited by 4 · depth 12 - ℂ-linearity of the Eichler–Shimura map
HeckeEis.existsEichlerShimuraMapLinear19 below · cited by 4 · depth 12 - Mod p Hecke eigenclass in parabolic cohomology of Γ₀(N)
HeckeEis.exists_coeffH1par_binaryFormRepSL_eigenclass_of_ideal_heckeAlgebra_of_ne_two54 below · cited by 1 · depth 12 - Split equivariant coefficient maps induce Hecke-equivariant maps on H¹ₚₐᵣ
HeckeEis.exists_coeffH1par_map_of_equivariant_retraction0 below · cited by 1 · depth 12 - Shapiro's lemma for parabolic cohomology, Hecke-equivariantly
HeckeEis.exists_coeffH1par_projLineRepSL_equiv_parabolicHoms9 below · cited by 1 · depth 12 - A conjugate-linear involution on parabolic cohomology
HeckeEis.exists_coeffH1par_semilinearMap_starRingEnd0 below · cited by 2 · depth 12 - Rational parabolic classes have nonzero integral multiples
HeckeEis.exists_ne_zero_smul_eq_coeffH1par_map_int_rat2 below · cited by 1 · depth 12 - Symᵖ⁻¹ as an equivariant summand of K[P¹(𝔽ₚ)]
HeckeEis.exists_retraction_binaryFormEval2 below · cited by 1 · depth 12 - Commutativity of the Hecke operators on Hom(Γ₀(N),A)
HeckeEis.heckeOperatorHom_commute0 below · cited by 1 · depth 12 - Kernel of level raising is Eisenstein for all T_ℓ
HeckeEis.heckeOperatorHom_eq_of_levelRaisingKernel32 below · cited by 1 · depth 12 - Degeneracy pullback ι₀^* commutes with T_ℓ
HeckeEis.heckeOperatorHom_pullback_iota00 below · cited by 1 · depth 12 - Hecke equivariance of the degeneracy pullback ι₁^* at ℓ ∤ q
HeckeEis.heckeOperatorHom_pullback_iota10 below · cited by 1 · depth 12 - Eichler–Shimura: images of ES and ̄ES are complementary
HeckeEis.isCompl_range_eichlerShimuraMap_range_conj638 below · cited by 1 · depth 12 - Rational independence in H¹ₚₐᵣ persists over ℂ
HeckeEis.linearIndependent_coeffH1par_map_rat_complex0 below · cited by 1 · depth 12 - Rational classes span parabolic cohomology over ℂ
HeckeEis.mem_span_range_coeffH1par_map_rat_complex0 below · cited by 1 · depth 12 - Naturality of `heckeOperatorHom` in the coefficient group
HeckeEis.postcomp_heckeOperatorHom0 below · cited by 6 · depth 12 - The central element -1 of SL₂(ℤ) acts by (-1)ⁿ
HeckeEis.binaryFormRepSL_neg_one_apply0 below · cited by 7 · depth 13 - Vanishing of parabolic H¹ for odd symmetric powers
HeckeEis.coeffH1par_binaryFormRepSL_eq_zero_of_odd1 below · cited by 1 · depth 13 - Cochain-level Hecke equivariance of the Shapiro map at ∞
HeckeEis.coeffHeckeFun_projLineAlphaAdj_apply_iota0_infty_eq_heckeOperatorHom4 below · cited by 1 · depth 13 - Additivity of the Eichler–Shimura map on cusp forms
HeckeEis.eichlerShimuraMap_add16 below · cited by 1 · depth 13 - Eichler–Shimura map computed by any admissible Eichler integral
HeckeEis.eichlerShimuraMap_eq_coeffH1parMk2 below · cited by 5 · depth 13 - Complex homogeneity of the Eichler–Shimura map
HeckeEis.eichlerShimuraMap_smul16 below · cited by 1 · depth 13 - Mod-p parabolic eigenclass attached to a maximal Hecke ideal
HeckeEis.exists_coeffH1par_int_modp_eigenclass_of_ideal_heckeAlgebra51 below · cited by 1 · depth 13 - Kernel of mod-p reduction on parabolic cohomology is p-divisible
HeckeEis.exists_eq_prime_smul_of_coeffH1par_map_eq_zero6 below · cited by 1 · depth 13 - Forms fixed by T^h are multiples of X₀ⁿ
HeckeEis.exists_eq_smul_X_pow_of_binaryFormRepSL_T_zpow_eq_self0 below · cited by 2 · depth 13 - Fixed forms of a lower unipotent are multiples of X₁ⁿ
HeckeEis.exists_eq_smul_X_pow_of_binaryFormRepSL_lowerUnipotent_eq_self1 below · cited by 1 · depth 13 - Existence of a parabolic Eichler integral for Γ₀(N) cusp forms
HeckeEis.exists_isEichlerIntegral_isParabolicCocycle12 below · cited by 6 · depth 13 - Parabolic characters of Γ₀(Np) come from parabolic cocycles
HeckeEis.exists_mem_coeffParabolicCocycles_forall_apply_infty_eq2 below · cited by 1 · depth 13 - Upper bound for parabolic H¹ of Γ₀(N) in binary forms
HeckeEis.finrank_coeffH1par_le_two_mul_dimFormula20 below · cited by 1 · depth 13 - Weight-two parabolic cohomology bound for Γ₀(N)
HeckeEis.finrank_coeffH1par_zero_le_two_mul_genusFormula21 below · cited by 1 · depth 13 - Eisenstein identity T_ℓ(χ∘ d)=(ℓ+1)(χ∘ d) for ℓ∤ N
HeckeEis.heckeOperatorHom_comp_gamma0UnitsChar5 below · cited by 2 · depth 13 - Kernel pairs of level raising are Eisenstein, given Ihara
HeckeEis.heckeOperatorHom_eq_of_kernelPair6 below · cited by 1 · depth 13 - Eichler integrals of cusp forms give parabolic cocycles
HeckeEis.isParabolicCocycle_cocycle_of_isEichlerIntegral7 below · cited by 3 · depth 13 - Weight identity j(g,τ)ⁿ(ρₙ(g)P)(1,-gτ)=P(1,-τ)
HeckeEis.jFactor_pow_mul_eval_binaryFormRepSL0 below · cited by 2 · depth 13 - Cocycles vanishing at ∞ on Γ₀(Np) are coboundaries
HeckeEis.mem_coeffCoboundaries_of_forall_apply_infty_eq_zero2 below · cited by 1 · depth 13 - Injectivity half of Eichler–Shimura for Γ₀(N)
HeckeEis.range_eichlerShimuraMap_inf_range_conj_eq_bot15 below · cited by 1 · depth 13 - Integral parabolic mod-p eigenclass attached to a Hecke eigenform
HeckeEis.exists_coeffH1par_int_modp_eigenclass_of_eigenform46 below · cited by 1 · depth 14 - Induced module Ind_{Γ_0(N)}^{SL₂(ℤ)} of binary forms: no invariants, no coinvariants
HeckeEis.exists_induced_binaryFormRepSL_top2 below · cited by 1 · depth 14 - Every Γ₀(N)-element is Γ₀(Np)-equivalent into U_N(ℓ)
HeckeEis.exists_iota0_inv_mul_mem_heckeUpper1 below · cited by 1 · depth 14 - Existence of Eichler integrals for holomorphic functions on H
HeckeEis.exists_isEichlerIntegral1 below · cited by 5 · depth 14 - The Hecke algebra of Sₙ₊₂(Γ₀(N)) is ℤ-finite
HeckeEis.finite_int_heckeAlgebra45 below · cited by 1 · depth 14 - Shapiro's lemma for parabolic cohomology: dimension inequality
HeckeEis.finrank_coeffH1par_gamma0_le_finrank_coeffH1par_top_induced1 below · cited by 1 · depth 14 - Dimension bound for parabolic cohomology of SL₂(ℤ)
HeckeEis.finrank_coeffH1par_top_add_le0 below · cited by 1 · depth 14 - Eisenstein eigenvalue ℓ+1 on entry-factoring homomorphisms of Γ₀(N)
HeckeEis.heckeOperatorHom_eq_of_factorsThroughEntry4 below · cited by 1 · depth 14 - Eichler integrals of slash-invariant f are equivariant primitives
HeckeEis.isEquivariantPrimitiveWith_of_isEichlerIntegral2 below · cited by 5 · depth 14 - Lower bounds for S- and ST-fixed binary forms
HeckeEis.le_finrank_fixed_S_and_ST_binaryFormRepSL0 below · cited by 1 · depth 14 - Fixed vectors in Ind_{Γ_0(N)}^{SL₂(ℤ)} of binary forms
HeckeEis.le_finrank_fixed_induced_binaryFormRepSL1 below · cited by 1 · depth 14 - p-saturation of the image of T^h-1 on integral binary forms
HeckeEis.mem_range_binaryFormRepSL_T_zpow_sub_one_of_prime_smul_mem0 below · cited by 1 · depth 14 - Hecke cochain is representative-independent modulo coboundaries
HeckeEis.sum_repr_sub_coeffHeckeFun_mem_coeffCoboundaries0 below · cited by 5 · depth 14 - X₁ⁿ-coefficient of a binary form as its value at (0,1)
HeckeEis.coeff_single_one_eq_eval_of_mem_binaryForm0 below · cited by 4 · depth 15 - Weight reduction to a ≤ p-1 for binary-form eigensystems
HeckeEis.exists_le_sub_one_isEigensystemH1_binaryFormRepSL_of_isEigensystemH18 below · cited by 1 · depth 15 - An SL₂(ℤ)-invariant pairing on binary forms of degree n
HeckeEis.exists_pairing_binaryForm_linePow0 below · cited by 1 · depth 15 - Characters through the lower-right entry are Eisenstein for T_ℓ
HeckeEis.heckeOperatorHom_apply_of_factorsThroughEntry3 below · cited by 1 · depth 15 - Scalar equivariance of the Hecke operator on characters
HeckeEis.heckeOperatorHom_smul0 below · cited by 1 · depth 15 - Eisenstein alternative for eigensystems on a Steinberg quotient
HeckeEis.isEigensystemH1_ind_comp_or_eisenstein_of_isEigensystemH1_of_steinberg_quotient8 below · cited by 1 · depth 15 - Characteristic 3: eigensystems lift from the Steinberg quotient or are Eisenstein
HeckeEis.isEigensystemH1_ind_comp_or_eisenstein_of_isEigensystemH1_of_steinberg_quotient_of_charP_three37 below · cited by 1 · depth 15 - Shapiro transfer of an eigensystem to trivial coefficients at level Nq
HeckeEis.isEigensystemH1_one_mul_of_isEigensystemH1_ind_comp5 below · cited by 1 · depth 15 - Forms with no X₁ⁿ term lie in the image of T^h-1
HeckeEis.mem_range_binaryFormRepSL_T_zpow_sub_one0 below · cited by 2 · depth 15 - Hecke equivariance of Eichler integrals on H¹(Γ₀(N),Symⁿ)
HeckeEis.coeffH1Mk_cocycle_heckeTLin_modularForm3 below · cited by 3 · depth 16 - Cochain-level Hecke multiplicativity T_ℓ T_{ℓ'} ≡ T_{ℓℓ'} modulo coboundaries
HeckeEis.coeffHeckeFun_coeffHeckeFun_sub_coeffHeckeFun_mul_mem_coeffCoboundaries2 below · cited by 10 · depth 16 - Cocycles on SL₂(ℤ) determined by z(S), z(ST)
HeckeEis.existsUnique_coeffCocycles_sl2z_apply_S_ST_eq0 below · cited by 5 · depth 16 - Transfer of Hecke eigenclasses from H¹(Γ₀(N),V) to Hom(Γ₀(Np),K)
HeckeEis.exists_addMonoidHom_functional_cocycle_smul_heckeOperatorHom_mul_eq2 below · cited by 3 · depth 16 - Mod-3 cocycles for Γ₀(N) come from integral ones
HeckeEis.exists_coeffCocycles_eq_sum_smul_map_intCast_add_three_of_exists_prime_dvd_mod_three_eq_two4 below · cited by 1 · depth 16 - Change of coefficients on H¹(Γ₀(N),Symⁿ) along a ring map
HeckeEis.exists_coeffH1_map_ringHom_binaryFormRepSL0 below · cited by 5 · depth 16 - Filtration of binary forms with Symᵃ⊗detᵇ subquotients, a≤ p-1
HeckeEis.exists_filtration_binaryForm_subquotient_le_sub_one2 below · cited by 1 · depth 16 - Injective mod p scalar extension of H¹(Γ₀(N),Symⁿ)
HeckeEis.exists_injective_baseChange_coeffH1_binaryFormRepSL1 below · cited by 2 · depth 16 - Eigensystems in H¹(Γ₀(N),Symⁿ) arise from weight n+2 forms
HeckeEis.exists_modularForm_heckeTLin_eq_smul_of_isEigensystemH1677 below · cited by 1 · depth 16 - From a Γ₀(N) eigensystem to a diamond-fixed eigenclass
HeckeEis.exists_ne_zero_map_conjHom_eq_and_heckeH1_gammaH_bot_eq_smul_of_isEigensystemH11 below · cited by 1 · depth 16 - Hecke operator acts by the index on conjugation-invariant characters
HeckeEis.heckeOperatorHom_apply_of_conj_invariant1 below · cited by 1 · depth 16 - Eichler–Shimura mod p: eigensystems occur in H¹(Γ₀(N),Symⁿ)
HeckeEis.isEigensystemH1_binaryFormRepSL_of_heckeTLin_eq_smul24 below · cited by 1 · depth 16 - Lifting Hecke eigensystems in H¹(Γ₀(N),·) along surjections
HeckeEis.isEigensystemH1_of_isEigensystemH1_of_surjective5 below · cited by 2 · depth 16 - Lifting a Hecke eigensystem along a surjection of coefficient modules
HeckeEis.isEigensystemH1_of_isEigensystemH1_of_surjective_of_subsingleton_H24 below · cited by 1 · depth 16 - Eigensystem lifts along an injection of coefficients, or is Eisenstein
HeckeEis.isEigensystemH1_or_of_isEigensystemH1_of_injective3 below · cited by 3 · depth 16 - No π-torsion in H¹(Γ₀(N), Symⁿ) when n<p
HeckeEis.mem_coeffCoboundaries_of_smul_mem_coeffCoboundaries_of_lt1 below · cited by 1 · depth 16 - Injectivity of Eichler–Shimura on Mₙ₊₂(Γ₀(N))
HeckeEis.modularForm_eq_zero_of_coeffH1Mk_cocycle_eq_zero7 below · cited by 2 · depth 16 - Integral cocycles span the K-valued cocycles for Γ₀(N)
HeckeEis.span_coeffCocycles_binaryFormRepSL_map_intCast_eq_top0 below · cited by 2 · depth 16 - Vanishing of Γ₀(N)-invariant binary forms of degree a<p
HeckeEis.eq_zero_of_forall_binaryFormRepSL_gamma0_eq_self0 below · cited by 1 · depth 17 - Binary forms vanishing on 𝔽ₚ² are divisible by Dickson's invariant
HeckeEis.exists_binaryForm_eq_mul_of_forall_eval_eq_zero0 below · cited by 1 · depth 17 - Divided a-th derivative partial₀ᵃ/X₁ᵃ with detᵃ-equivariance
HeckeEis.exists_dividedDeriv_binaryFormRep_eq_det_pow_smul0 below · cited by 1 · depth 17 - Hecke-equivariant Eichler–Shimura decomposition of parabolic cohomology
HeckeEis.exists_eichlerShimura_coeffH1par_binaryFormRepSL645 below · cited by 1 · depth 17 - Partial Hecke eigensystems on H¹(Γ₀(N),Symⁿ) extend to full ones
HeckeEis.exists_isEigensystemH1_binaryFormRepSL_empty_of_isEigensystemH1_of_ringHom6 below · cited by 1 · depth 17 - Ash–Stevens reduction to weight two, level dividing Np²
HeckeEis.exists_isEigensystemH1_one_dvd_mul_sq_of_isEigensystemH1_binaryFormRepSL17 below · cited by 1 · depth 17 - Boundary Hecke eigensystems arise from modular forms
HeckeEis.exists_modularForm_heckeTLin_eq_smul_of_notMem_range_coeffH1parToH143 below · cited by 1 · depth 17 - Residual H¹ eigensystem at level N from a cuspidal type
HeckeEis.isEigensystemH1_of_H1_gammaH_dual_of_isCuspidalOfType_of_qCoeff_congr47 below · cited by 1 · depth 17 - Steinberg-quotient eigensystems pass between fields of characteristic p
HeckeEis.isEigensystemH1_steinberg_quotient_of_isEigensystemH1_steinberg_quotient_of_charP8 below · cited by 1 · depth 17 - Diagonal element intertwines Hecke conjugation with reduction mod q
HeckeEis.diagElem_comp_comp_red_heckeConj_eq_comp_red_comp_diagElem_of_ne_zero0 below · cited by 3 · depth 18 - Semilinear change of coefficients on Γ₀(N)-coefficient cohomology
HeckeEis.exists_addMonoidHom_coeffH1_of_equivariant_addMonoidHom0 below · cited by 2 · depth 18 - Integral basis of coefficient cohomology with integral Hecke matrices
HeckeEis.exists_basis_coeffH1_eq_and_mem_span_and_exists_matrix_of_basis_eq0 below · cited by 2 · depth 18 - Newform eigensystem in H¹ with dual cuspidal-type coefficients
HeckeEis.exists_coeffH1_dual_ne_zero_isCoeffHeckeOnH1_eq_qCoeff_smul_of_isCuspidalOfType42 below · cited by 1 · depth 18 - Hecke-equivariant embedding of coefficient H¹ into Γ_{H_1}(Nq²)-cohomology
HeckeEis.exists_coeffH1_restrict_injective_range_iff_equivariant_heckeT_of_charZero5 below · cited by 3 · depth 18 - Ash–Stevens weight reduction to weight two with nebentypus
HeckeEis.exists_isEigensystemH1_gamma0NebenRep_of_isEigensystemH1_binaryFormRepSL_of_dvd5 below · cited by 1 · depth 18 - Twisting a mod-p nebentypus eigensystem to trivial nebentypus
HeckeEis.exists_isEigensystemH1_one_of_isEigensystemH1_gamma0NebenRep13 below · cited by 1 · depth 18 - Cocycles for Γ₀(N): Eichler–Shimura plus parabolic
HeckeEis.exists_modularForm_coeffCocycles_sub_cocycle_mem_coeffParabolicCocycles19 below · cited by 1 · depth 18 - Level raising at q for H¹ eigensystems when q+1 ≠ 0
HeckeEis.isEigensystemH1_binaryFormRepSL_mul_of_isEigensystemH15 below · cited by 1 · depth 18 - Base change of an H¹ Hecke eigensystem along a field embedding
HeckeEis.isEigensystemH1_of_isEigensystemH1_of_isBaseChange2 below · cited by 2 · depth 18 - Hecke eigensystem in H¹ descends to the residue field
HeckeEis.isEigensystemH1_residueField_of_isEigensystemH1_of_isDiscreteValuationRing4 below · cited by 1 · depth 18 - Mod-3 twist of a weight-two eigensystem, level divided by 3M
HeckeEis.exists_isEigensystemH1_one_natCast_mul_of_isEigensystemH1_one_of_three_dvd8 below · cited by 1 · depth 19 - Eisenstein eigensystem ℓ↦ℓ+1 in H¹(Γ₀(M),κ)
HeckeEis.isEigensystemH1_one_natCast_add_one6 below · cited by 1 · depth 19 - Vanishing cusp values force parabolicity of Γ₀(N)-cocycles
HeckeEis.mem_coeffParabolicCocycles_of_forall_coeff_binaryFormRepSL_inv_apply_eq_zero3 below · cited by 1 · depth 19 - Mod-3 cocycle bd· x on Γ₀(M) is a coboundary
HeckeEis.exists_map_mul_eq_add_add_upperRightMulLowerRight_mul_of_three_dvd1 below · cited by 1 · depth 20
HeckeEis.IsEichlerIntegral 10
- Eichler integrals under integral matrices of positive determinant
HeckeEis.IsEichlerIntegral.binarySubst_adjugate_comp_smul0 below · cited by 3 · depth 13 - Eichler integral with constant evaluation at (1,-τ) integrates zero
HeckeEis.IsEichlerIntegral.eq_zero_of_eval_eq_const2 below · cited by 2 · depth 13 - Bol's identity one rung at a time
HeckeEis.IsEichlerIntegral.hasDerivAt_eval_iterate_pderiv0 below · cited by 3 · depth 13 - Boundedness at i∞ of a T^h-equivariant Eichler integral's evaluation
HeckeEis.IsEichlerIntegral.isBoundedAtImInfty_eval4 below · cited by 2 · depth 13 - Eichler integrals transform under SL₂(ℤ)
HeckeEis.IsEichlerIntegral.slash0 below · cited by 6 · depth 13 - Additivity of the Eichler integral relation
HeckeEis.IsEichlerIntegral.add0 below · cited by 1 · depth 14 - Eichler integrals of the same form differ by a constant
HeckeEis.IsEichlerIntegral.exists_sub_eq_const0 below · cited by 4 · depth 14 - Eichler integrals scale: cF is an Eichler integral of cf
HeckeEis.IsEichlerIntegral.smul0 below · cited by 1 · depth 14 - Parabolic condition for Eichler integrals at ∞
HeckeEis.IsEichlerIntegral.vadd_sub_T_zpow_apply_mem_range3 below · cited by 1 · depth 14 - Period of an Eichler integral around a cusp
HeckeEis.IsEichlerIntegral.coeff_binaryFormRepSL_inv_apply_sub_eq_intervalIntegral_slash2 below · cited by 1 · depth 19