normalize_coe_nat — Mathlib

English

For every natural number n, the integer embedding n maps to itself under normalization: normalize(n) = n.

Русский

Для каждого натурального числа n нормализация отображает n как само число: normalize(n) = n.

LaTeX

$$$$\operatorname{normalize}(n) = n \quad (n \in \mathbb{N}).$$$$

Lean4

theorem normalize_coe_nat (n : ℕ) : normalize (n : ℤ) = n :=
  normalize_of_nonneg (ofNat_le_ofNat_of_le <| Nat.zero_le n)

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