norm_nonneg — Mathlib

English

If d ≤ 0, then for every element n ∈ Z√d, we have 0 ≤ norm(n).

Русский

Если $d \\le 0$, то для каждого элемента $n \\in \\mathbb{Z} \\sqrt{d}$ выполняется $0 \\le \\operatorname{norm}(n)$.

LaTeX

$$(d \\le 0) \\Rightarrow \\forall n \\in \\mathbb{Z}\\sqrt{d}, \\ 0 \\le \\operatorname{norm}(n)$$

Lean4

theorem norm_nonneg (hd : d ≤ 0) (n : ℤ√d) : 0 ≤ n.norm :=
  add_nonneg (mul_self_nonneg _)
    (by
      rw [mul_assoc, neg_mul_eq_neg_mul]
      exact mul_nonneg (neg_nonneg.2 hd) (mul_self_nonneg _))

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