instNeg — Mathlib

English

There is a negation operation on cusp forms: the negation of a cusp form is a cusp form.

Русский

Существует операция отрицания над cusp forms: -f является cusp-form.

LaTeX

$$$-f \in \mathrm{CuspForm}(\Gamma,k)$ if $f \in \mathrm{CuspForm}(\Gamma,k)$, and \(-(f) = -f$ as forms.$$

Lean4

instance instNeg : Neg (CuspForm Γ k) :=
  ⟨fun f =>
    { toSlashInvariantForm := -f.1
      holo' := f.holo'.neg
      zero_at_cusps' hc g hg := by simpa using (f.zero_at_cusps' hc g hg).neg }⟩

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