Absolute values and the integers

This file contains some results on absolute values applied to integers.

Main results

• AbsoluteValue.map_units_int: an absolute value sends all units of ℤ to 1

@[simp]

theorem AbsoluteValue.map_units_int {S : Type u_2} [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] (abv : AbsoluteValue ℤ S) (x : ℤˣ) : abv ↑x = 1

@[simp]

theorem AbsoluteValue.map_units_intCast {R : Type u_1} {S : Type u_2} [Ring R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] [Nontrivial R] (abv : AbsoluteValue R S) (x : ℤˣ) : abv ↑↑x = 1

@[simp]

theorem AbsoluteValue.map_units_int_smul {R : Type u_1} {S : Type u_2} [Ring R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S] (abv : AbsoluteValue R S) (x : ℤˣ) (y : R) : abv (x • y) = abv y