Documentation

Mathlib.Analysis.NormedSpace.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‖₊.

theorem Int.norm_coe_units (e : ˣ) :
e = 1
@[simp]
theorem Int.nnnorm_coe_nat (n : ) :
n‖₊ = n
@[simp]