Theorems · Definition · number theory
ModularForm.toSlashInvariantForm
{Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → ModularForm Γ k → SlashInvariantForm Γ kThe SlashInvariantForm associated to a ModularForm.
- Defined in
- Mathlib.NumberTheory.ModularForms.Basic
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Matrixstatement · cited by 4,303
- Subgroupstatement and proof · cited by 3,593
- Matrix.GeneralLinearGroupstatement and proof · cited by 556
- ModularFormstatement and proof · cited by 98
- SlashInvariantFormstatement · cited by 46
Cited by13
Results whose statement or proof uses this declaration.
- ModularForm.mulproof · cited by 6
- ModularForm.toCuspFormproof · cited by 4
- CuspForm.translateproof · cited by 3
- ModularForm.holo'statement · cited by 3
- CuspForm.mulModularFormproof · cited by 1
- ModularForm.bdd_at_cusps'statement · cited by 1
- ModularForm.isZeroAt_of_coeffZero_eq_zeroproof · cited by 1
- CuspForm.traceproof · cited by 1
- ModularForm.toFun_eq_coestatement · cited by 0
- ModularForm.toSlashInvariantForm_coestatement · cited by 0
- ModularForm.toSlashInvariantForm_intCaststatement · cited by 0
- ModularForm.toSlashInvariantForm_natCaststatement · cited by 0