exists_norm_eq_mul_self

Mathlib.Analysis.Complex.Basic

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

English

For every z ∈ ℂ there exists a unit c with ‖c‖ = 1 such that ‖z‖ = c z.

Русский

Для каждого z ∈ ℂ существует единичный фактор c с ‖c‖ = 1 such that ‖z‖ = c z.

LaTeX

$$$\\\\exists c, \\\\|c\\\\| = 1 \\\\land \\\\|z\\\\| = c \\\\cdot z$$$

Lean4

theorem exists_norm_eq_mul_self (z : ℂ) : ∃ c, ‖c‖ = 1 ∧ ‖z‖ = c * z :=
  RCLike.exists_norm_eq_mul_self _

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

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

Разделы

Аффилиация

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