exists_norm_eq_mul_self — Mathlib

English

For any x ∈ K, there exists a unit c with ||c|| = 1 such that ↑||x|| = c x (i.e., a unit modulus scalar aligns x with its norm embedded in K).

Русский

Для любого x ∈ K существует единичный модульный множитель c с ||c|| = 1 such, что ↑||x|| = c x (то есть x может быть приведено к своему нормированному значению при помощи единичного множителя).

LaTeX

$$$$ \exists c, \|c\| = 1 \\land \\uparrow\|x\| = c x. $$$$

Lean4

theorem exists_norm_eq_mul_self (x : K) : ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x :=
  by
  obtain rfl | hx := eq_or_ne x 0
  · exact ⟨1, by simp⟩
  · exact ⟨‖x‖ / x, by simp [norm_ne_zero_iff.2, hx]⟩

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