norm_add_eq

Mathlib.Analysis.Complex.Arg

URI: https://scilib.ai/kg/mathlib#Complex.norm_add_eq

English

If x.arg = y.arg, then ∥x+y∥ = ∥x∥ + ∥y∥.

Русский

Если x.arg = y.arg, то ∥x+y∥ = ∥x∥ + ∥y∥.

LaTeX

$$$$\text{If } x.\arg = y.\arg, \ \|x+y\| = \|x\| + \|y\|.$$$$

Lean4

theorem norm_add_eq (h : x.arg = y.arg) : ‖x + y‖ = ‖x‖ + ‖y‖ :=
  (sameRay_of_arg_eq h).norm_add

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

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

Разделы

Аффилиация

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