abs_to_nat — Mathlib

English

For every ZNum n, the natural cast of abs n equals Int.natAbs n.

Русский

Для каждого ZNum n натуральное приведение abs n равно Int.natAbs n.

LaTeX

$$$$\forall n:\mathrm{ZNum},\ (\lvert n \rvert:\mathbb{N}) = \operatorname{Int.natAbs}(n).$$$$

Lean4

@[simp]
theorem abs_to_nat : ∀ n, (abs n : ℕ) = Int.natAbs n
  | 0 => rfl
  | pos p => congr_arg Int.natAbs p.to_nat_to_int
  | neg p => show Int.natAbs ((p : ℕ) : ℤ) = Int.natAbs (-p) by rw [p.to_nat_to_int, Int.natAbs_neg]

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