three_lt_four_mul_im_sq_of_mem_fdo

Mathlib.NumberTheory.Modular

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

← MathLib Explorer

English

If z ∈ 𝒟ᵒ, then 3 < 4 (Im z)^2.

Русский

Если z ∈ 𝒟ᵒ, то 3 < 4 (Im z)^2.

LaTeX

$$$z\\in 𝒟^{\\circ} \\Rightarrow 3 < 4(\\Im z)^2.$$$

Lean4

theorem three_lt_four_mul_im_sq_of_mem_fdo (h : z ∈ 𝒟ᵒ) : 3 < 4 * z.im ^ 2 :=
  by
  have : 1 < z.re * z.re + z.im * z.im := by simpa [Complex.normSq_apply] using h.1
  have := h.2
  cases abs_cases z.re <;> nlinarith

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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