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.
‖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