zero_apply

Mathlib.NumberTheory.ModularForms.Basic

URI: https://scilib.ai/kg/mathlib#CuspForm.zero_apply

English

For z in the upper half-plane, the zero cusp form evaluates to zero: (0 : CuspForm Γ k)(z) = 0.

Русский

Для z на верхней полуплоскости нулевая cusp-form оценивается как нуль: (0 : CuspForm Γ k)(z) = 0.

LaTeX

$$$\forall z \in \mathbb{H}, \; (0 : \mathrm{CuspForm}(\Gamma,k))(z) = 0.$$

Lean4

@[simp]
theorem zero_apply (z : ℍ) : (0 : CuspForm Γ k) z = 0 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru