normalize_of_nonpos — Mathlib

English

If z is nonpositive, then normalization sends z to its negation: normalize(z) = −z when z ≤ 0.

Русский

Если z неположительно, то нормализация отправляет z в −z: normalize(z) = −z при z ≤ 0.

LaTeX

$$$z \le 0 \implies \operatorname{normalize}(z) = -z$$$

Lean4

theorem normalize_of_nonpos {z : ℤ} (h : z ≤ 0) : normalize z = -z :=
  by
  obtain rfl | h := h.eq_or_lt
  · simp
  · rw [normalize_apply, normUnit_eq, if_neg (not_le_of_gt h), Units.val_neg, Units.val_one, mul_neg_one]

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