sub_apply — Mathlib

English

Let f and g be cusp forms of weight k for the group Γ. Then for every z in the upper half-plane, (f − g)(z) = f(z) − g(z).

Русский

Пусть f и g — cusp-функции весa k для группы Γ. Тогда для каждого z из верхней полуплоскости имеет место (f − g)(z) = f(z) − g(z).

LaTeX

$$$\forall \Gamma, k, f,g:\mathrm{CuspForm}(\Gamma,k),\ \forall z\in\mathbb{H},\ (f-g)(z)=f(z)-g(z)$$$

Lean4

@[simp]
theorem sub_apply (f g : CuspForm Γ k) (z : ℍ) : (f - g) z = f z - g z :=
  rfl

Похожие утверждения