toSlashInvariantForm_intCast — Mathlib

English

For any Γ with det ±1, casting an integer to a modular form and taking its slash-invariant form yields the same integer as a slash-invariant form.

Русский

Для любой Γ с det ±1 приведение числа к модулярной форме и получение его slash-инвариантной формы даёт то же число в виде slash-инвариантной формы.

LaTeX

$$$\forall {\Gamma} [\GammaHasDetPlusMinusOne] (z : \mathbb{Z}), (z : \mathrm{ModularForm}(\Gamma,0)).\mathrmtoSlashInvariantForm = z.$$

Lean4

theorem toSlashInvariantForm_intCast [Γ.HasDetPlusMinusOne] (z : ℤ) : (z : ModularForm Γ 0).toSlashInvariantForm = z :=
  rfl

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