English
The set of modular forms is closed under addition; the sum is again a modular form of the same subgroup and weight, with natural componentwise addition of values and cusp-holomorphic data.
Русский
Множество модульных форм замкнуто по сложению; сумма продолжает быть модульной формой той же подгруппы и веса, значения суммируются по Коши-компонентам и данные в точках бесконечностей сохраняются.
LaTeX
$$$f,g \in \mathrm{ModularForm}(\Gamma,k) \Rightarrow f+g \in \mathrm{ModularForm}(\Gamma,k)$$$
Lean4
instance add : Add (ModularForm Γ k) where
add f
g :=
{ toSlashInvariantForm := f + g
holo' := f.holo'.add g.holo'
bdd_at_cusps' hc := by simpa using (f.bdd_at_cusps' hc).add (g.bdd_at_cusps' hc) }
