norm_le_im_iff_eq_I_mul_norm — Mathlib

English

For any z ∈ K, ||z|| ≤ im z holds if and only if z = I · ||z||; assuming the appropriate I conditions.

Русский

Для любого z ∈ K неравенство ||z|| ≤ im z эквивалентно z = I · ||z|| при заданных условиях на I.

LaTeX

$$$$ \\text{norm\_le\_im\_iff\_eq\_I\_mul\_norm} \\{z : K\\} : \\|z\\| \\le \\operatorname{im}(z) \\;\\iff\\; z = I \\cdot \\|z\\|. $$$$

Lean4

theorem norm_le_im_iff_eq_I_mul_norm {z : K} : ‖z‖ ≤ im z ↔ z = I * ‖z‖ :=
  by
  obtain (h | h) := I_eq_zero_or_im_I_eq_one (K := K)
  · simp [h, im_eq_zero]
  · have : (I : K) ≠ 0 := fun _ ↦ by simp_all
    rw [← mul_right_inj' (neg_ne_zero.mpr this)]
    convert norm_le_re_iff_eq_norm (z := -I * z) using 2
    all_goals simp [neg_mul, ← mul_assoc, I_mul_I_of_nonzero this, norm_I_of_ne_zero this]

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