norm_add_eq_iff — Mathlib

English

For complex numbers x,y, ∥x+y∥ = ∥x∥ + ∥y∥ if and only if x and y are nonzero with the same argument (i.e., same ray), or one of them is zero.

Русский

Для комплексных чисел x,y выполняется ∥x+y∥ = ∥x∥ + ∥y∥ тогда и только тогда, когда x и y принадлежат одной луче или один из них равен нулю.

LaTeX

$$$$\|x+y\| = \|x\| + \|y\| \iff x=0 \lor y=0 \lor x.arg = y.arg.$$$$

Lean4

theorem norm_add_eq_iff : ‖x + y‖ = ‖x‖ + ‖y‖ ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg :=
  sameRay_iff_norm_add.symm.trans sameRay_iff

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