coe_natCast — Mathlib

English

Let Γ be a subgroup with determinant ±1. For every natural number n, the modular form n of weight 0 is the constant function with value n on the upper half-plane.

Русский

Пусть Γ является подгруппой с детерминантом ±1. Для любого натурального числа n модулярная форма n веса 0 есть константная функция на верхней полуплоскости со значением n.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem coe_natCast [Γ.HasDetPlusMinusOne] (n : ℕ) : ⇑(n : ModularForm Γ 0) = n :=
  rfl

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