IsZeroAt — Mathlib

English

A function vanishes at a cusp under SL(2,ℤ) translates if and only if all translates vanish at infinity.

Русский

Функция обращается в ноль в стыке при переносах SL(2,ℤ) тогда и только тогда, когда все переносы сходны к нулю в бесконечности.

LaTeX

$$$\\text{IsZeroAt}(c,f,k) := \\forall g, g·∞=c \\Rightarrow \\text{IsZeroAtImInfty}(f|[k]g)$$$

Lean4

/-- We say `f` is zero at `c` if, for all `g` with `g • ∞ = c`, the function `f ∣[k] g` is
zero at `∞`. -/
def IsZeroAt : Prop :=
  ∀ g : GL (Fin 2) ℝ, g • ∞ = c → IsZeroAtImInfty (f ∣[k] g)

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