Theorems · Theorem · number theory
ModularForm.discriminant_bounded_factor
Deprecated since 2026-04-30Use ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_pow instead.
Filter.Tendsto (fun x => ∏' (n : ℕ), (1 - ModularForm.eta_q n ↑x) ^ 24) UpperHalfPlane.atImInfty (nhds 1)
Alias of ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_pow.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 286 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement · cited by 5,565
- nhdsstatement · cited by 5,554
- Filter.Tendstostatement · cited by 3,814
- SummationFilter.unconditionalstatement · cited by 2,068
- UpperHalfPlanestatement · cited by 626
- UpperHalfPlane.coestatement · cited by 288
- tprodstatement · cited by 230
- UpperHalfPlane.atImInftystatement · cited by 35
- ModularForm.eta_qstatement · cited by 15
- ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_powproof · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.