denom_J

Mathlib.NumberTheory.ModularForms.Basic

URI: https://scilib.ai/kg/mathlib#UpperHalfPlane.denom_J

English

For every τ in the upper half-plane, the denominator associated to J and τ is equal to 1.

Русский

Для каждого τ из верхней полуплоскости знаменатель, соответствующий J и τ, равен 1.

LaTeX

$$$\operatorname{denom} J \tau = 1$$$

Lean4

@[simp]
theorem denom_J (τ : ℍ) : denom J τ = 1 := by simp [J, denom]

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

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

Разделы

Аффилиация

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