r_pos

Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

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

English

For every z in the upper half-plane, r(z) > 0.

Русский

Для каждого z в верхней полуплоскости верно r(z) > 0.

LaTeX

$$$\\forall z \\in \\mathbb{H},\\; 0 < r(z)$$$

Lean4

theorem r_pos : 0 < r z := by simp only [r, lt_min_iff, im_pos, Real.sqrt_pos, r1_pos, and_self]

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

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

Разделы

Аффилиация

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