lean_workbook_plus_60633

Proved

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

Prove that if $z_n=a_n+i\cdot b_n$ for $n=1,2,3,...,k$ .\nThen the inequality is just $|z_1+z_2+...+z_k|\le |z_1|+|z_2|+...+|z_n|$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60633 : ∀ k : ℕ, ∀ z : Fin k → ℂ, ‖∑ i : Fin k, z i‖ ≤ ∑ i : Fin k, ‖z i‖   :=  by sorry

Source