eq_coe_norm_of_nonneg — Mathlib

English

If z ∈ ℂ is nonnegative in the ComplexOrder (i.e., z ≥ 0), then z equals its real embedding of the norm: z = ↑‖z‖.

Русский

Если z ∈ ℂ неотрицательно по ComplexOrder, то z равно комплексному числу, полученному из нормы: z = ↑‖z‖.

LaTeX

$$$0 \\le z \\Rightarrow z = \\uparrow \\|z\\|$$$

Lean4

theorem eq_coe_norm_of_nonneg {z : ℂ} (hz : 0 ≤ z) : z = ↑‖z‖ :=
  by
  lift z to ℝ using hz.2.symm
  rw [norm_real, Real.norm_of_nonneg (id hz.1 : 0 ≤ z)]

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