ext — Mathlib

English

Two modular forms are equal if they have equal values at every point of the upper half-plane.

Русский

Две модулярные формы равны, если их значения в каждой точке верхней полуплоскости совпадают.

LaTeX

$$$\forall f,g : \mathrm{ModularForm}(\Gamma,k),\; (\forall z \in \mathbb{H}, f(z)=g(z)) \Rightarrow f=g$$$

Lean4

@[ext]
theorem ext {f g : ModularForm Γ k} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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