feat(data/int): absolute values and integers (#9028)

We prove that an absolute value maps all `units ℤ` to `1`.

I added a new file since there is no neat place in the import hierarchy where this fit (the meet of `algebra.algebra.basic` and `data.int.cast`).

Author: Vierkantor

src/data/int/absolute_value.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2021 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import algebra.absolute_value
+import algebra.algebra.basic
+import data.int.cast
+import group_theory.group_action.units
+
+/-!
+# Absolute values and the integers
+
+This file contains some results on absolute values applied to integers.
+
+## Main results
+
+ * `absolute_value.map_units_int`: an absolute value sends all units of `ℤ` to `1`
+-/
+
+variables {R S : Type*} [ring R] [linear_ordered_comm_ring S]
+
+@[simp]
+lemma absolute_value.map_units_int (abv : absolute_value ℤ S) (x : units ℤ) :
+  abv x = 1 :=
+by rcases int.units_eq_one_or x with (rfl | rfl); simp
+
+@[simp]
+lemma absolute_value.map_units_int_cast [nontrivial R] (abv : absolute_value R S) (x : units ℤ) :
+  abv ((x : ℤ) : R) = 1 :=
+by rcases int.units_eq_one_or x with (rfl | rfl); simp
+
+@[simp]
+lemma absolute_value.map_units_int_smul (abv : absolute_value R S) (x : units ℤ) (y : R) :
+  abv (x • y) = abv y :=
+by rcases int.units_eq_one_or x with (rfl | rfl); simp