coe_neg

Mathlib.NumberTheory.ModularForms.Basic

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

English

The function underlying the negation of a cusp form is the negation of the function itself.

Русский

Основанная функция для -f равна - f(z).

LaTeX

$$$\forall f:\mathrm{CuspForm}(\Gamma,k), \; \mathrm{coe}(-f) = -\mathrm{coe}(f).$$$

Lean4

@[simp]
theorem coe_neg (f : CuspForm Γ k) : ⇑(-f) = -f :=
  rfl

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

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

Разделы

Аффилиация

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