exists_norm_mul_eq_self

Mathlib.Analysis.Complex.Basic

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

English

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

Русский

Для каждого z ∈ ℂ существует единичный множитель c с ‖c‖ = 1, удовлетворяющий c · ‖z‖ = z.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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