toSlashInvariantForm_natCast — Mathlib

English

Let Γ be a subgroup with det ±1. For every n ∈ ℕ, the slash-invariant form arising from the constant modular form n is the constant slash-invariant form with value n.

Русский

Пусть Γ — подгруппа с det ±1. Для каждого n ∈ ℕ slash-инвариантная форма, ассоциированная с константной модулярной формой n, является константной slash-инвариантной формой со значением n.

LaTeX

$$$\forall {\Gamma} [\GammaHasDetPlusMinusOne] \ (n : \mathbb{N}): (n : \mathrm{ModularForm}(\Gamma,0)).\mathrm{toSlashInvariantForm} = n.$$

Lean4

theorem toSlashInvariantForm_natCast [Γ.HasDetPlusMinusOne] (n : ℕ) : (n : ModularForm Γ 0).toSlashInvariantForm = n :=
  rfl

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