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ℤ
to1
@[simp]
theorem
absolute_value.map_units_int
{S : Type u_2}
[linear_ordered_comm_ring S]
(abv : absolute_value ℤ S)
(x : ℤˣ) :
@[simp]
theorem
absolute_value.map_units_int_cast
{R : Type u_1}
{S : Type u_2}
[ring R]
[linear_ordered_comm_ring S]
[nontrivial R]
(abv : absolute_value R S)
(x : ℤˣ) :
@[simp]
theorem
absolute_value.map_units_int_smul
{R : Type u_1}
{S : Type u_2}
[ring R]
[linear_ordered_comm_ring S]
(abv : absolute_value R S)
(x : ℤˣ)
(y : R) :