Prove2Me

lean_workbook_plus_48236

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Suppose that z1,z2,⋯zn∈Cz_1,z_2,\cdots z_n\in{\mathbb{C}} then ∣z1∣+∣z2∣+⋯+∣zn∣≥∣z1+z2+⋯+zn∣ |z_1|+|z_2|+\cdots +|z_n|\ge|z_1+z_2+\cdots+z_n| holds.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48236 : ∀ n : ℕ, ∀ z : Fin n → ℂ, ∑ i, ‖z i‖ ≥ ‖∑ i, z i‖   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph