feat(analysis/normed_space/int): norms of (units of) integers (#8136)

From LTE

src/analysis/normed_space/int.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2021 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import analysis.normed_space.basic
+
+/-!
+# 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∥₊`.
+-/
+
+open_locale big_operators
+
+namespace int
+
+lemma nnnorm_coe_units (e : units ℤ) : ∥(e : ℤ)∥₊ = 1 :=
+begin
+  obtain (rfl|rfl) := int.units_eq_one_or e;
+  simp only [units.coe_neg_one, units.coe_one, nnnorm_neg, nnnorm_one],
+end
+
+lemma norm_coe_units (e : units ℤ) : ∥(e : ℤ)∥ = 1 :=
+by rw [← coe_nnnorm, int.nnnorm_coe_units, nnreal.coe_one]
+
+@[simp] lemma nnnorm_coe_nat (n : ℕ) : ∥(n : ℤ)∥₊ = n := real.nnnorm_coe_nat _
+
+@[simp] lemma norm_coe_nat (n : ℕ) : ∥(n : ℤ)∥ = n := real.norm_coe_nat _
+
+@[simp] lemma to_nat_add_to_nat_neg_eq_nnnorm (n : ℤ) : ↑(n.to_nat) + ↑((-n).to_nat) = ∥n∥₊ :=
+by rw [← nat.cast_add, to_nat_add_to_nat_neg_eq_nat_abs, nnreal.coe_nat_abs]
+
+@[simp] lemma to_nat_add_to_nat_neg_eq_norm (n : ℤ) : ↑(n.to_nat) + ↑((-n).to_nat) = ∥n∥ :=
+by simpa only [nnreal.coe_nat_cast, nnreal.coe_add]
+  using congr_arg (coe : _ → ℝ) (to_nat_add_to_nat_neg_eq_nnnorm n)
+
+end int

src/data/fintype/basic.lean

@@ -692,6 +692,8 @@ instance : fintype bool := ⟨⟨tt ::ₘ ff ::ₘ 0, by simp⟩, λ x, by cases
 instance units_int.fintype : fintype (units ℤ) :=
 ⟨{1, -1}, λ x, by cases int.units_eq_one_or x; simp *⟩
 
+@[simp] lemma units_int.univ : (finset.univ : finset (units ℤ)) = {1, -1} := rfl
+
 instance additive.fintype : Π [fintype α], fintype (additive α) := id
 
 instance multiplicative.fintype : Π [fintype α], fintype (multiplicative α) := id

src/data/int/basic.lean

@@ -1071,6 +1071,16 @@ lemma pred_to_nat : ∀ (i : ℤ), (i - 1).to_nat = i.to_nat - 1
 lemma to_nat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.to_nat - 1 : ℕ) : ℤ) = i - 1 :=
 by simp [h, le_of_lt h] with push_cast
 
+@[simp] lemma to_nat_sub_to_nat_neg : ∀ (n : ℤ), ↑n.to_nat - ↑((-n).to_nat) = n
+| (0 : ℕ)   := rfl
+| (n+1 : ℕ) := show ↑(n+1) - (0:ℤ) = n+1, from sub_zero _
+| -[1+ n]   := show 0 - (n+1 : ℤ)  = _,   from zero_sub _
+
+@[simp] lemma to_nat_add_to_nat_neg_eq_nat_abs : ∀ (n : ℤ), (n.to_nat) + ((-n).to_nat) = n.nat_abs
+| (0 : ℕ)   := rfl
+| (n+1 : ℕ) := show (n+1) + 0 = n+1, from add_zero _
+| -[1+ n]   := show 0 + (n+1) = n+1, from zero_add _
+
 /-- If `n : ℕ`, then `int.to_nat' n = some n`, if `n : ℤ` is negative, then `int.to_nat' n = none`.
 -/
 def to_nat' : ℤ → option ℕ