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.nnnorm_coe_units (e : ℤˣ) : ‖↑e‖₊ = 1

theorem Int.norm_coe_units (e : ℤˣ) : ‖↑e‖ = 1

@[simp]

theorem Int.nnnorm_natCast (n : ℕ) : ‖↑n‖₊ = ↑n

@[deprecated Int.nnnorm_natCast (since := "2024-04-05")]

theorem Int.nnnorm_coe_nat (n : ℕ) : ‖↑n‖₊ = ↑n

Alias of Int.nnnorm_natCast.

@[simp]

theorem Int.toNat_add_toNat_neg_eq_nnnorm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖₊

@[simp]

theorem Int.toNat_add_toNat_neg_eq_norm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖