← all areas

Namespace ModularForm 156 theorems

Landmarks here: Vanishing of weight-2 cusp forms of level 2 · Weight-two cusp forms of level one vanish

— 153 · AtkinLehnerDatum 3

directly in ModularForm 153

• landmark Vanishing of weight-2 cusp forms of level 2 ModularForm.S2_Gamma0_2_eq_zero 0 below · cited by 2 · depth 4
• landmark Weight-two cusp forms of level one vanish ModularForm.S2_Gamma0_one_eq_zero 0 below · cited by 2 · depth 6
• f∣_k W is Γ₀(M)-invariant when f is ModularForm.alSlash_slash_eq_self_of_mem_Gamma0 0 below · cited by 0 · depth 9
• A simultaneous Hecke eigen-sequence with a₁=0 vanishes ModularForm.eq_zero_of_coeffHecke_eigen_of_apply_one_eq_zero 0 below · cited by 3 · depth 9
• Boundedness at cusps is preserved by f ↦ f∣_k W_q ModularForm.isBoundedAt_alSlash 0 below · cited by 0 · depth 9
• Weight-2 trace f+U_q(f∣ W_q) is Γ₀(R)-invariant ModularForm.add_heckeU_alSlash_slash_eq_self_of_mem_Gamma0 0 below · cited by 0 · depth 10
• Atkin–Lehner trace identity for f∣_k W_q ModularForm.alSlash_add_heckeU_alSlash_alSlash 0 below · cited by 4 · depth 10
• Atkin–Lehner operator commutes with T_ℓ, ℓ∤ M ModularForm.alSlash_heckeT_comm 0 below · cited by 6 · depth 10
• Coefficient operators Tₚ and U_q commute for coprime p,q ModularForm.coeffHeckeT_coeffHeckeU_comm 0 below · cited by 2 · depth 10
• Coefficient Hecke operators commute at coprime levels ModularForm.coeffHeckeT_comm 0 below · cited by 2 · depth 10
• Commutativity of the coefficient operators Uₚ and U_q ModularForm.coeffHeckeU_comm 0 below · cited by 2 · depth 10
• Hecke eigenvalues of a normalised eigen-sequence are its prime coefficients ModularForm.coeffHecke_eigenvalue_eq_apply_of_apply_one_eq_one 0 below · cited by 2 · depth 10
• Tₚ with diamond correction preserves Γ₁(N)-invariance ModularForm.heckeU_add_slash_heckeDiagMatrix_slash_eq_of_mem_Gamma1 0 below · cited by 2 · depth 10
• Vanishing at cusps of f + U_q(f∣_k W_q) ModularForm.isZeroAt_add_heckeU_alSlash 0 below · cited by 0 · depth 10
• Holomorphy of f + U_q(f∣_k W_q) ModularForm.mdifferentiable_add_heckeU_alSlash 0 below · cited by 0 · depth 10
• Sturm bound for Γ₀(N) modular forms ModularForm.sturm_bound_Gamma0 6 below · cited by 9 · depth 10
• Integrality of the coefficient-level Hecke operator Tₚ ModularForm.coeffHeckeT_int 0 below · cited by 1 · depth 11
• Integrality of the coefficient operator Uₚ ModularForm.coeffHeckeU_int 0 below · cited by 1 · depth 11
• Weight-2 transformation of η(z)²η(11z)² under Γ₀(11) ModularForm.etaProductEleven_transform 8 below · cited by 1 · depth 11
• Finite-dimensionality of M_k(G) for arithmetic G ModularForm.finiteDimensional_of_isArithmetic 4 below · cited by 6 · depth 11
• Tₚ preserves Γ₀(N)-invariance for p ∤ N ModularForm.heckeT_slash_eq_self_of_mem_Gamma0 0 below · cited by 1 · depth 11
• Uₚ preserves weight-k invariance under Γ₀(N) ModularForm.heckeU_slash_eq_self_of_mem_Gamma0 0 below · cited by 1 · depth 11
• Boundedness at i∞ is preserved by Tₚ ModularForm.isBoundedAtImInfty_heckeT 0 below · cited by 5 · depth 11
• Boundedness at i∞ is preserved by Uₚ ModularForm.isBoundedAtImInfty_heckeU 0 below · cited by 6 · depth 11
• Holomorphy of Tₚ f for holomorphic f ModularForm.mdifferentiable_heckeT 0 below · cited by 6 · depth 11
• Holomorphy of Uₚ f on the upper half-plane ModularForm.mdifferentiable_heckeU 0 below · cited by 24 · depth 11
• 1-periodicity of Tₚ f ModularForm.periodic_heckeT_comp_ofComplex 0 below · cited by 5 · depth 11
• Uₚ preserves 1-periodicity ModularForm.periodic_heckeU_comp_ofComplex 0 below · cited by 15 · depth 11
• Sturm bound for arithmetic subgroups with period one ModularForm.sturm_bound_of_isArithmetic 5 below · cited by 2 · depth 11
• Double Atkin–Lehner slash acts as the scalar q^{k-2} ModularForm.alSlash_alSlash 0 below · cited by 10 · depth 12
• Vanishing twisted trace forces F∣ W_q = -U_q F ModularForm.alSlash_eq_neg_heckeU_of_trace_alSlash_eq_zero 1 below · cited by 1 · depth 12
• Sturm bound at width M for arithmetic groups ModularForm.eq_zero_of_lt_order_qExpansion_of_isArithmetic 2 below · cited by 2 · depth 12
• 1-periodicity of η(z)²η(11z)² ModularForm.etaProductEleven_add_one 2 below · cited by 1 · depth 12
• Weight-24 transformation of (η(τ)²η(11τ)²)¹² on Γ₀(11) ModularForm.etaProductEleven_pow_twelve_smul 2 below · cited by 2 · depth 12
• Weight-two transformation of η(τ)²η(11τ)² when c=11b ModularForm.etaProductEleven_smul_of_apply_one_zero_eq 5 below · cited by 1 · depth 12
• A level-one form is a form for Γ₀(N) ModularForm.exists_gamma0_qExpansion_eq_of_levelOne 1 below · cited by 13 · depth 12
• First Rankin–Cohen bracket of modular forms ModularForm.exists_rankinCohen_one_qExpansion_eq 75 below · cited by 11 · depth 12
• T_ℓ-eigenvalue of the W_q-twisted trace combination ModularForm.heckeT_trace_alSlash_of_eigen 13 below · cited by 1 · depth 12
• Integrality of ̃ g/Δ̃^{ m} over ℂ[jmath̃] ModularForm.isIntegral_adjoin_qExpansion_div_discriminant_pow_of_isArithmetic 1 below · cited by 6 · depth 12
• p-integral Eisenstein coefficients divisible by p when (p-1)∣ k ModularForm.eisenstein_qCoeff_p_integral_dvd 0 below · cited by 4 · depth 13
• q-product expansion of η(z)²η(11z)² ModularForm.etaProductEleven_eq_qParam_mul_tprod 1 below · cited by 1 · depth 13
• Fricke eigenvalue -1 for η(w)²η(11w)² ModularForm.etaProductEleven_fricke 2 below · cited by 1 · depth 13
• Degeneracy map f(τ)↦ f(dτ) from Γ₀(M) to Γ₀(N) ModularForm.exists_degeneracy_Gamma0 0 below · cited by 19 · depth 13
• Modular forms on Γ₀(N) separate inequivalent points ModularForm.exists_gamma0_apply_mul_apply_ne_of_forall_smul_ne 1 below · cited by 2 · depth 13
• E₄³/Δ as a ratio of weight-12 forms on Γ₀(ℓ) ModularForm.exists_gamma0_qExpansion_div_eq_E4_cube_div_discriminant 1 below · cited by 3 · depth 13
• Ratios of modular forms are algebraic over ℂ(jmath̃) ModularForm.exists_polynomial_aeval_qExpansion_div_eq_zero_of_isArithmetic 1 below · cited by 4 · depth 13
• Level one: weight 12N forms are P(j) Δ^N in ℂ((q)) ModularForm.exists_qExpansion_eq_aeval_mul_pow_levelOne 0 below · cited by 8 · depth 13
• Vanishing at cusps is preserved under the Atkin–Lehner slash ModularForm.isZeroAt_alSlash 0 below · cited by 2 · depth 13
• Level-one vanishing from q-expansion order at width M ModularForm.levelOne_eq_zero_of_lt_order_qExpansion 0 below · cited by 1 · depth 13
• Holomorphy of the Atkin–Lehner slash f∣_k W ModularForm.mdifferentiable_alSlash 0 below · cited by 2 · depth 13
• q-expansion of τ↦ F(Nτ) for level-one F ModularForm.qExpansion_heckeDiagMatrix_smul_eq_qExpand_of_levelOne 3 below · cited by 18 · depth 13
• M ∣ 12b₀ for constant reductions on Γ₀(p) ModularForm.dvd_twelve_mul_qCoeff_zero_of_forall_dvd_qCoeff 558 below · cited by 1 · depth 14
• Square of the S-transformation of η ModularForm.eta_neg_one_div_sq 1 below · cited by 1 · depth 14
• Slashing a Γ_H(N)-form by an element of Γ₀(N) ModularForm.exists_coe_eq_slash_of_mem_gamma0_gammaH 0 below · cited by 4 · depth 14
• Tₚ preserves the weight-k nebentypus law on Γ₀(N) ModularForm.heckeU_add_smul_slash_heckeDiagMatrix_slash_of_mem_Gamma0 0 below · cited by 3 · depth 14
• Uₚ lowers the level from Γ₀(N) to Γ₀(N/p) when p² ∣ N ModularForm.heckeU_slash_eq_self_of_mem_Gamma0_div 0 below · cited by 3 · depth 14
• A weight-two form on Γ₀(p) constant mod ℓ is 0 mod ℓ ModularForm.dvd_qCoeff_zero_of_prime_ne_level_dvd_qCoeff 15 below · cited by 1 · depth 15
• Translation of η by an integer ModularForm.eta_add_intCast 0 below · cited by 2 · depth 15
• Dedekind's η transformation law for c>0 ModularForm.eta_specialLinearGroup_smul 4 below · cited by 1 · depth 15
• T_ℓ acts as 1+ℓ^{k-1} modulo cusp forms ModularForm.exists_cuspForm_coeffHeckeT_eq_of_modEq_one 2 below · cited by 2 · depth 15
• Division of modular forms: Φ/Ψ is a cusp form ModularForm.exists_cuspForm_mul_eq_of_analyticOrderAt_le 0 below · cited by 2 · depth 15
• Level-p to level-one trace of a modular form ModularForm.exists_levelOne_coe_eq_zpow_smul_add_heckeU_slash_fricke 0 below · cited by 8 · depth 15
• Weight four level one: a₁ = 240 a₀ ModularForm.levelOne_weight_four_qCoeff_one 0 below · cited by 10 · depth 15
• Level-one weight-14 forms with vanishing constant term are zero ModularForm.levelOne_weight_fourteen_qCoeff_eq_zero 0 below · cited by 3 · depth 15
• Weight six level one: a₁ = -504 a₀ ModularForm.levelOne_weight_six_qCoeff_one 0 below · cited by 10 · depth 15
• Level-one weight-12 forms with vanishing constant term are τ-multiples ModularForm.levelOne_weight_twelve_qCoeff_eq_qCoeff_one_mul_discriminant 0 below · cited by 10 · depth 15
• Weight two on Γ₀(p): 9∣ bₙ (n≥1) forces 3∣ b₀ ModularForm.three_dvd_qCoeff_zero_of_nine_dvd_qCoeff 528 below · cited by 1 · depth 15
• 2 ∣ b₀ for weight-two forms on Γ₀(p) with 8 ∣ bₙ ModularForm.two_dvd_qCoeff_zero_of_eight_dvd_qCoeff 546 below · cited by 1 · depth 15
• Continuity of the canonical logarithm of η ModularForm.continuous_logEta 0 below · cited by 4 · depth 16
• Integrality of (p+1)a₀ for weight-two forms on Γ₀(p) ModularForm.dvd_succ_mul_qCoeff_zero_of_dvd_qCoeff 9 below · cited by 2 · depth 16
• The S-transformation law of η: η(-1/z)=√-iz η(z) ModularForm.eta_modular_S_smul 0 below · cited by 2 · depth 16
• Serre derivative sends weight k forms on Γ₀(N) to weight k+2 ModularForm.exists_gamma0_coe_eq_serreDerivative 0 below · cited by 2 · depth 16
• Existence of a weight p-1 form on Γ₀(N') congruent to 1 mod p ModularForm.exists_gamma0_qCoeff_intCast_and_dvd_sub_one_of_five_le 0 below · cited by 4 · depth 16
• Congruent form with integral q-expansion modulo 𝔪 ModularForm.exists_isIntegralQExp_qCoeff_congr_of_qCoeff_congr_intCast_gammaH 105 below · cited by 1 · depth 16
• Weight-two Γ₀(p) form congruent to a constant modulo m ModularForm.exists_katzModularForm_qExpansion_eq_C_of_dvd_qCoeff 526 below · cited by 1 · depth 16
• Level-one forms from symmetric functions of Γ₀(p)-translates ModularForm.exists_levelOne_esymm_qExpansion_congr_of_gamma0_two 3 below · cited by 1 · depth 16
• Hecke's weight-one Eisenstein series for an odd primitive character ModularForm.exists_weightOne_eisenstein_qCoeff_eq_of_isPrimitive_of_odd 4 below · cited by 5 · depth 16
• η has a canonical logarithm on H ModularForm.exp_logEta 0 below · cited by 4 · depth 16
• Finite-dimensionality of M_k(Γ₀(N)) ModularForm.finiteDimensional_Gamma0 5 below · cited by 3 · depth 16
• Hecke operators Tₚ, T_q on M_k(Γ₀(N)) commute ModularForm.heckeTLin_comm 7 below · cited by 3 · depth 16
• Γ_H(M)-invariance of U_ℓ plus the diamond-twisted term ModularForm.heckeU_add_slash_slash_eq_self_of_mem_GammaH 0 below · cited by 3 · depth 16
• U_q preserves weight-k Γ_H(M)-invariance when q ∣ M ModularForm.heckeU_slash_eq_self_of_mem_GammaH 0 below · cited by 3 · depth 16
• Integer translation law for the logarithm of η ModularForm.logEta_add_intCast 0 below · cited by 2 · depth 16
• Dedekind's η transformation law in logarithmic form ModularForm.logEta_specialLinearGroup_smul 7 below · cited by 3 · depth 16
• Integrality at the cusp 0 via a peaked auxiliary form ModularForm.qExpansion_slash_coeff_mem_of_peaked_auxiliary 12 below · cited by 1 · depth 16
• Forms with integral q-expansion span M_k(Γ₀(N)) ModularForm.span_setOf_qCoeff_intCast_eq_top 104 below · cited by 1 · depth 16
• Swinnerton-Dyer weight congruence: (ℓ-1) ∣ k ModularForm.sub_one_dvd_weight_of_qExpansion_congr_const_levelOne 10 below · cited by 1 · depth 16
• Parity of the constant term when p ≡ 7 (mod 8) ModularForm.two_dvd_qCoeff_zero_of_eight_dvd_qCoeff_of_mod_eight_eq_seven 539 below · cited by 1 · depth 16
• Regularity, rationality and Galois transport for wp at torsion ModularForm.weierstrassP_torsion_qExpansion_package 1 below · cited by 2 · depth 16
• Mazur's constant q-expansion principle at prime level ModularForm.dvd_twelve_mul_qCoeff_zero_and_dvd_qCoeff_mul_of_dvd_qCoeff 538 below · cited by 1 · depth 17
• Weight-four Eisenstein series with partial divisor-sum q-expansions ModularForm.exists_gamma1_weight_four_isIntegralQExp_partialDivisorSum_slash_eq 2 below · cited by 2 · depth 17
• Level-one forms are isobaric in E₄,E₆ mod ℓ≥ 5 ModularForm.exists_isWeightedHomogeneous_aeval_eq_map_qExpansion_levelOne 4 below · cited by 1 · depth 17
• Weight-two Γ₀(p) forms as Katz forms over ℤ[1/p] ModularForm.exists_katzGamma0Form_evalCusp_eq_of_five_le 499 below · cited by 2 · depth 17
• Trace of an even-weight modular form to level one ModularForm.exists_levelOne_coe_eq_sum_slash 0 below · cited by 1 · depth 17
• Integral level-one forms E₄ᵃE₆ᵇ of weight 4a+6b ModularForm.exists_levelOne_qExpansion_eq_map_int_constantCoeff_one 0 below · cited by 1 · depth 17
• Fricke matrix acts as -Uₚ in weight two ModularForm.heckeU_add_slash_fricke_eq_zero 0 below · cited by 2 · depth 17
• Level-one forms of weight 12N: first N+1 coefficients determine integrality ModularForm.levelOne_qExpansion_coeff_mem_of_coeff_le_mem 4 below · cited by 1 · depth 17
• Logarithmic S-transformation law for logη ModularForm.logEta_modular_S_smul 3 below · cited by 1 · depth 17
• The Atkin–Lehner slash is multiplicative up to a factor q ModularForm.alSlash_mul 0 below · cited by 2 · depth 18
• Integrality of weight-two Γ₀(p) q-expansions over level one ModularForm.exists_mvPolynomial_levelOne_relation_qExpansion_gamma0_of_weight_two 6 below · cited by 1 · depth 18
• Finite-dimensionality and Sturm bound for M_k(G) ModularForm.finiteDimensional_and_finrank_le_of_isArithmetic 7 below · cited by 4 · depth 18
• q-expansion coefficients of Fricke-rational forms on Γ₁(N) ModularForm.gamma1_qExpansion_coeff_mem_of_frickeRational 9 below · cited by 2 · depth 18
• Rational basis for M_k(Γ₁(N)) ModularForm.exists_basis_gamma1_qCoeff_mem_range_ratCast 41 below · cited by 1 · depth 19
• Prescribing constant terms at all cusps of Γ₀(N) ModularForm.exists_gamma0_forall_tendsto_slash_atImInfty_of_three_le 0 below · cited by 1 · depth 19
• Weight-two forms on Γ₀(N) with prescribed cusp values ModularForm.exists_gamma0_weight_two_forall_tendsto_slash_atImInfty 5 below · cited by 1 · depth 19
• Rational level-one forms are isobaric polynomials in E₄, E₆ ModularForm.exists_isWeightedHomogeneous_aeval_eq_of_map_eq_qExpansion_levelOne 2 below · cited by 1 · depth 19
• Integral weight-2m forms on Γ₀(N) attaining the dimension bound ModularForm.exists_linearIndependent_int_qCoeff_dimFormula_le_card 793 below · cited by 1 · depth 19
• A weight-one form on Γ₁(3) with Fricke eigenvalue -i/√3 ModularForm.exists_weight_one_gamma1_three_slash_fricke_eq_smul 2 below · cited by 1 · depth 19
• Holomorphy is preserved by slashing with diag(d,1) ModularForm.mdifferentiable_slash_heckeDiagMatrix 0 below · cited by 1 · depth 19
• Slash by diag(d,1) carries Γ₀(R)-invariance to Γ₀(M) ModularForm.rescaleSlash_slash_eq_self_of_mem_Gamma0 0 below · cited by 1 · depth 19
• Basis of M_k(Γ₁(N)) with coefficients in ℚ(ζ_N) ModularForm.exists_basis_gamma1_qCoeff_mem_adjoin_exp 33 below · cited by 1 · depth 20
• Galois equivariance of ℚ(ζ_N)-rational forms on Γ₁(N) ModularForm.exists_gamma1_qCoeff_eq_algEquiv_apply 27 below · cited by 1 · depth 20
• Weight-two forms on Γ(N) with prescribed cusp values ModularForm.exists_gamma_weight_two_forall_tendsto_slash_atImInfty 4 below · cited by 1 · depth 20
• First Rankin–Cohen bracket of E₄ and Δ ModularForm.qExpansion_E4_mul_theta_discriminant_sub 76 below · cited by 1 · depth 20
• Even-weight forms on Γ₁(N) have a ℚ(ζ_N)-rational basis ModularForm.exists_basis_gamma1_qCoeff_mem_adjoin_exp_of_even 29 below · cited by 1 · depth 21
• Galois transport of K-rational modular forms on Γ₁(N), even weight ModularForm.exists_gamma1_qCoeff_eq_algEquiv_apply_of_even 23 below · cited by 1 · depth 21
• Division of modular forms on Γ₀(N) ModularForm.exists_modularForm_mul_eq_of_analyticOrderAt_le 0 below · cited by 1 · depth 21
• Jacobi's identity for E₄ η⁸ in eta quotients ModularForm.E4_mul_eta_pow_eight_eq 19 below · cited by 1 · depth 22
• Jacobi's quartic identity in eta form ModularForm.eta_pow_twentyfour_eq 16 below · cited by 1 · depth 22
• Level-one modular forms restrict to any subgroup of SL₂(ℤ) ModularForm.exists_coe_eq_of_levelOne 0 below · cited by 4 · depth 22
• Division of modular forms: Φ/Ψ is a cusp form ModularForm.exists_cuspForm_mul_eq_of_forall_analyticOrderAt_le 0 below · cited by 1 · depth 22
• Galois transport of Fricke-rational modular forms on Γ₁(N) ModularForm.exists_gamma1_frickeRational_sigmaTransport 16 below · cited by 1 · depth 22
• Recognition criterion for weight-k forms via E₄ᵃE₆ᵇ/Δ^m ModularForm.exists_mul_E4_pow_mul_E6_pow_eq_iff 2 below · cited by 3 · depth 22
• Rational fractions in j and Fricke functions span M_k(Γ) ModularForm.span_frickeRational_E4_pow_E6_pow_eq_top 22 below · cited by 1 · depth 22
• A level-one form read at 2z lies on Γ₀(4) ModularForm.exists_gamma0_four_apply_eq_apply_two_smul 0 below · cited by 1 · depth 23
• Weight-one form on Γ₁(M) congruent to 1 modulo 2 ModularForm.exists_gamma1_weightOne_qCoeff_intCast_and_two_dvd_sub_one 6 below · cited by 2 · depth 23
• Forms on Γ_H(N) separate inequivalent points ModularForm.exists_gammaH_apply_mul_apply_ne_of_forall_smul_ne 17 below · cited by 1 · depth 23
• Mod p congruence between weights k+1 and k on Γ₁(p) ModularForm.exists_isIntegralQExp_gamma1_weight_add_one_map_zmod_eq 5 below · cited by 4 · depth 23
• Integral q-expansions of E₄ and E₆ on Γ₁(M) ModularForm.exists_gamma1_isIntegralQExp_eisenstein_four_six 0 below · cited by 3 · depth 24
• Forms on Γ_H(N) separate points of one Γ₀(N)-orbit ModularForm.exists_gammaH_apply_mul_apply_ne_of_forall_smul_ne_of_gamma0_smul_eq 15 below · cited by 1 · depth 24
• An eta-product identity for E₄ at level four ModularForm.E4_mul_etaProduct_eq 20 below · cited by 1 · depth 25
• Powers of a Γ₀(M)-permuted family of Γ₁(M)-forms ModularForm.exists_gamma1_coe_eq_pow_of_forall_slash_eq 0 below · cited by 1 · depth 25
• H-symmetrisation of a Γ₀(M)-permuted family of Γ₁(M)-forms ModularForm.exists_gammaH_coe_eq_sum_of_forall_slash_eq 1 below · cited by 1 · depth 25
• Invariance of f∣ W + Uₚ f at level R ModularForm.alSlash_add_heckeU_slash_eq_self_of_mem_GammaH 0 below · cited by 3 · depth 26
• A Γ_H(M)-invariant form for Γ₁(M) is modular for Γ_H(M) ModularForm.exists_gammaH_coe_eq_of_forall_slash_eq 0 below · cited by 1 · depth 26
• Lower bound for dim M_k(Γ₁(M)), k≥ 3, M≥ 5 ModularForm.exists_linearIndependent_gamma1_dimFormula_le_card 515 below · cited by 1 · depth 26
• Mod p q-expansion principle for Γ₀(M)-translates ModularForm.exists_qCoeff_slash_eq_mul_of_forall_qCoeff_eq_mul_of_prime_not_dvd 103 below · cited by 1 · depth 26
• An eta-product identity for 16E₄ at level 4 ModularForm.sixteen_mul_E4_mul_eta_quarter_pow_eq 20 below · cited by 1 · depth 26
• Even-weight dimension lower bound for M_k(Γ₁(M)) ModularForm.exists_linearIndependent_gamma1_dimFormula_le_card_of_even 472 below · cited by 1 · depth 27
• Odd-weight dimension lower bound for M_k(Γ₁(M)) ModularForm.exists_linearIndependent_gamma1_dimFormula_le_card_of_odd 513 below · cited by 1 · depth 27
• Weight-one form on Γ₁(M) with v vartheta j = w² ModularForm.exists_gamma1_weightOne_ne_zero_and_mul_thetaL_eq_qExpansion_sq 90 below · cited by 1 · depth 28
• Conjugate translates of forms on Γ₁(M)∩Γ₀(Mp) stay algebraic ModularForm.exists_coe_eq_slash_and_qExpansion_coeff_mem_range_of_mem_gamma0_of_mul_eq 99 below · cited by 1 · depth 29
• Division of modular forms on a finite-index subgroup ModularForm.exists_modularForm_mul_eq_of_analyticOrderAt_le_of_finiteIndex 0 below · cited by 2 · depth 29
• H-invariant ratios of forms on G become ratios on H ModularForm.exists_mul_eq_mul_norm_of_forall_slash_mul_eq 0 below · cited by 29 · depth 29
• Independence of the Atkin–Lehner slash on Γ_H(M) ModularForm.alSlash_eq_alSlash_of_gammaH 0 below · cited by 1 · depth 30
• Finite order of a non-zero modular form at a cusp ModularForm.exists_tendsto_slash_div_qParam_pow_of_conj_T_pow_mem 0 below · cited by 1 · depth 30
• Atkin–Lehner slash as a diamond followed by diag(p,1) ModularForm.alSlash_coe_eq_coe_diamondLinH_slash_heckeDiagMatrix 3 below · cited by 3 · depth 32
• Atkin–Lehner twist of T_ℓ on Γ_H(M)-invariant functions ModularForm.heckeU_add_slash_alSlash_eq_alSlash_heckeU_add_slash_of_not_dvd 0 below · cited by 1 · depth 33
• Atkin–Lehner conjugation turns U_{q'} into its transpose ModularForm.heckeU_alSlash_eq_alSlash_sum_slash_transpose_of_dvd_div 0 below · cited by 2 · depth 33
• p-integrality of Atkin–Lehner expansions at cofactor M/p ModularForm.exists_not_dvd_and_forall_isIntegral_mul_qExpansion_alSlash_of_isIntegralQExp_of_even 358 below · cited by 2 · depth 34
• Atkin–Lehner slash preserves level-Γ_H(M) modular forms ModularForm.exists_GammaH_coe_eq_alSlash_of_forall_unitsMap_atkinLehnerFactor_eq_one 1 below · cited by 1 · depth 35
• Trace intertwines twisted Atkin–Lehner with Fricke involution ModularForm.exists_coe_eq_slash_mul_alGL_and_coe_trace_slash_eq_coe_trace 2 below · cited by 1 · depth 37
• Serre's valuation lemma for the level-lowering trace ModularForm.exists_map_eq_qExpansion_smul_trace_mul_pow_and_map_eq_of_slash_alGL_inv 3 below · cited by 1 · depth 37

ModularForm.AtkinLehnerDatum 3

• Existence of an Atkin–Lehner datum at a prime exactly dividing the level ModularForm.AtkinLehnerDatum.nonempty_of_prime_of_dvd_of_not_sq_dvd 0 below · cited by 22 · depth 9
• The Atkin–Lehner prime q does not divide the cofactor R ModularForm.AtkinLehnerDatum.not_dvd_R_of_prime 0 below · cited by 1 · depth 16
• The Atkin–Lehner matrix normalises Γ₀(M) ModularForm.AtkinLehnerDatum.exists_mem_Gamma0_alGL_mul_eq 0 below · cited by 13 · depth 26