English
The constant function with value x ∈ ℂ gives a modular form of weight 0 for any Γ with det = ±1; its value is constantly x.
Русский
Постоянная функция со значением x ∈ ℂ является модульной формой веса 0 для любого Γ; значение постоянно равно x.
LaTeX
$$$ (\mathrm{const}(x))(z) = x \quad \text{for all } z. $$$
Lean4
/-- The constant function with value `x : ℂ` as a modular form of weight 0 and any level. -/
def const (x : ℂ) [Γ.HasDetOne] : ModularForm Γ 0
where
toSlashInvariantForm := .const x
holo' _ := mdifferentiableAt_const
bdd_at_cusps' hc g
hg := by
simpa only [const_toFun, slash_def, SlashInvariantForm.toFun_eq_coe, Function.const_apply, neg_zero,
zpow_zero] using atImInfty.const_boundedAtFilter _
