abs_two_mul_re_lt_one_of_mem_fdo

Mathlib.NumberTheory.Modular

URI: https://scilib.ai/kg/mathlib#ModularGroup.abs_two_mul_re_lt_one_of_mem_fdo

English

If z ∈ 𝒟ᵒ, then |2 z.re| < 1.

Русский

Если z ∈ 𝒟ᵒ, то |2 z.re| < 1.

LaTeX

$$$z\\in 𝒟^{\\circ} \\Rightarrow |2 z_{\\Re}| < 1.$$$

Lean4

theorem abs_two_mul_re_lt_one_of_mem_fdo (h : z ∈ 𝒟ᵒ) : |2 * z.re| < 1 :=
  by
  rw [abs_mul, abs_two, ← lt_div_iff₀' (zero_lt_two' ℝ)]
  exact h.2

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

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

Разделы

Аффилиация

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