English
If a modular form of weight k is constant with value c, then either k = 0 or c = 0.
Русский
Если модульная форма веса k является константой со значением c, то либо k = 0, либо c = 0.
LaTeX
$$$ \text{If } f(z) = c \text{ is a modular form of weight } k \text{ for } \Gamma(1), \text{ then } k = 0 \lor c = 0.$$$
Lean4
/-- If a constant function is modular of weight `k`, then either `k = 0`, or the constant is `0`. -/
theorem wt_eq_zero_of_eq_const {f : F} {c : ℂ} (hf : ⇑f = Function.const _ c) : k = 0 ∨ c = 0 :=
by
have hI := slash_action_eqn_SL'' f (mem_Gamma_one S) I
have h2I2 := slash_action_eqn_SL'' f (mem_Gamma_one S) ⟨2 * Complex.I, by simp⟩
simp_rw [sl_moeb, hf, Function.const, denom_S, coe_mk_subtype] at hI h2I2
nth_rw 1 [h2I2] at hI
simp only [mul_zpow, coe_I, mul_eq_mul_right_iff, mul_left_eq_self₀] at hI
refine hI.imp_left (Or.casesOn · (fun H ↦ ?_) (False.elim ∘ zpow_ne_zero k I_ne_zero))
rwa [← ofReal_ofNat, ← ofReal_zpow, ← ofReal_one, ofReal_inj, zpow_eq_one_iff_right₀ (by simp) (by simp)] at H
