mathlib documentation

analysis.normed_space.int

The integers as normed ring #

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.norm_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∥