lean_workbook_plus_14972
DisprovedSince , we have .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14972 : ∀ z : ℂ, ‖z‖ < 1 / 2 → 2 * ‖z‖ ^ 2 ≤ ‖z‖ ^ 2 := by sorry
Source
Since , we have .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14972 : ∀ z : ℂ, ‖z‖ < 1 / 2 → 2 * ‖z‖ ^ 2 ≤ ‖z‖ ^ 2 := by sorry