Theorems · Theorem · number theory

SlashInvariantForm.wt_eq_zero_of_eq_const

∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (k : ℤ)
  [SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] {f : F} {c : ℂ},
  ⇑f = Function.const UpperHalfPlane c → k = 0 ∨ c = 0

If a constant function is modular of weight k, then either k = 0, or the constant is 0.

Defined in

Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Cited by

1 results in Mathlib

Foundations

Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FunLikeSlashInvariantFormClass