one_coe_eq_one

Mathlib.NumberTheory.ModularForms.SlashInvariantForms

URI: https://scilib.ai/kg/mathlib#SlashInvariantForm.one_coe_eq_one

English

The function associated to the unit form is the constant function 1.

Русский

Функция, соответствующая единице формы, является константной единицей.

LaTeX

$$$\big((1 : \mathrm{SlashInvariantForm}(\Gamma,0)) : \mathbb{H} \to \mathbb{C}\big) = 1.$$$

Lean4

@[simp]
theorem one_coe_eq_one [Γ.HasDetPlusMinusOne] : ((1 : SlashInvariantForm Γ 0) : ℍ → ℂ) = 1 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru