r1_eq

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

URI: https://scilib.ai/kg/mathlib#EisensteinSeries.r1_eq

English

Let z lie in the upper half-plane. Then r1(z) equals 1 divided by ((Re z)/(Im z))^2 + 1.

Русский

Пусть z принадлежит верхней полуплоскости. Тогда r1(z) = 1 / ((Re z)/(Im z))^2 + 1.

LaTeX

$$$ r_1(z) = \\dfrac{1}{\\left( \\dfrac{\\operatorname{Re} z}{\\operatorname{Im} z} \\right)^2 + 1}$$$

Lean4

theorem r1_eq : r1 z = 1 / ((z.re / z.im) ^ 2 + 1) := by rw [div_pow, div_add_one (by positivity), one_div_div, r1]

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

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

Разделы

Аффилиация

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