Theorems · Definition · number theory
ModularForm.discriminant
UpperHalfPlane → ℂ
The modular discriminant Δ(z) = η(z) ^ 24, where η is the Dedekind eta function.
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement · cited by 5,565
- UpperHalfPlanestatement and proof · cited by 626
- UpperHalfPlane.coeproof · cited by 288
- ModularForm.etaproof · cited by 6
Cited by22
Results whose statement or proof uses this declaration.
- CuspForm.discriminantEquivproof · cited by 8
- CuspForm.discriminantproof · cited by 7
- ModularForm.discriminant_eq_q_prodstatement · cited by 4
- ModularForm.discriminant_ne_zerostatement · cited by 2
- ModularForm.discriminant_qExpansion_coeff_onestatement and proof · cited by 2
- ModularForm.qExpansion_eq_qExpansion_discriminant_mulstatement and proof · cited by 1
- CuspForm.coe_discriminantstatement · cited by 1
- ModularForm.discriminant_cuspFunction_eqOnstatement and proof · cited by 1
- ModularForm.sturm_bound_levelOne_natproof · cited by 1
- ModularForm.discriminant_isZeroAtImInftystatement · cited by 1
- ModularForm.discriminant_mul_discriminantEquivstatement · cited by 1
- ModularForm.discriminant_qExpansion_orderstatement and proof · cited by 1