normSq_pos — Mathlib

English

For every z ∈ ℂ, the squared modulus is positive if and only if z ≠ 0: 0 < |z|^2 ⇔ z ≠ 0.

Русский

Для каждого z ∈ ℂ, квадрат модуля положителен тогда и только тогда, когда z ≠ 0: 0 < |z|^2 ⇔ z ≠ 0.

LaTeX

$$$0 < \\\\|z\\\\|^2 \\\\iff z \\\\neq 0$$$

Lean4

@[simp]
theorem normSq_pos {z : ℂ} : 0 < normSq z ↔ z ≠ 0 :=
  (normSq_nonneg z).lt_iff_ne.trans <| not_congr (eq_comm.trans normSq_eq_zero)

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