coe_intCast — Mathlib

English

Let Γ be a subgroup with det ±1. For every z ∈ ℤ, the underlying function of z cast to ModularForm Γ 0 equals z.

Русский

Пусть Γ — подгруппа с det ±1. Для каждого z ∈ ℤ функция, лежащая в основе z как модульная форма, равна z.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_intCast [Γ.HasDetPlusMinusOne] (z : ℤ) : ⇑(z : ModularForm Γ 0) = z :=
  rfl

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