The integers as normed ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains basic facts about the integers as normed ring.

Recall that ‖n‖ denotes the norm of n as real number. This norm is always nonnegative, so we can bundle the norm together with this fact, to obtain a term of type nnreal (the nonnegative real numbers). The resulting nonnegative real number is denoted by ‖n‖₊.

source

theorem int.nnnorm_coe_units (e : ℤ ˣ) :

‖↑e‖₊ = 1

source

theorem int.norm_coe_units (e : ℤ ˣ) :

‖↑e‖ = 1

source

@[simp]

theorem int.nnnorm_coe_nat (n : ℕ) :

‖↑n‖₊ = ↑n

source

@[simp]

theorem int.to_nat_add_to_nat_neg_eq_nnnorm (n : ℤ) :

↑(n.to_nat) + ↑((-n).to_nat) = ‖n‖₊

source

@[simp]

theorem int.to_nat_add_to_nat_neg_eq_norm (n : ℤ) :

↑(n.to_nat) + ↑((-n).to_nat) = ‖n‖