Theorems · Theorem · number theory
ModularForm.levelOne_odd_weight_eq_zero
∀ {k : ℤ}, Odd k → ∀ (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k), f = 0A 𝒮ℒ modular form of odd weight is zero (evaluate at -1 ∈ SL(2, ℤ)).
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- map_oneproof · cited by 861
- Matrix.GeneralLinearGroupstatement · cited by 556
- Matrix.extproof · cited by 540
- Oddstatement and proof · cited by 364
- Matrix.SpecialLinearGroupstatement · cited by 348
- MonoidHom.rangestatement and proof · cited by 314
- Int.castRingHomproof · cited by 254
- Matrix.SpecialLinearGroup.mapGLstatement and proof · cited by 98
- ModularFormstatement and proof · cited by 98
- Units.extproof · cited by 86
Cited by1
Results whose statement or proof uses this declaration.
- ModularForm.levelOne_odd_weight_rank_zeroproof · cited by 0