Absolute values and the integers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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ℤto1int.nat_abs_hom:int.nat_absbundled as amonoid_with_zero_hom
@[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) :
int.nat_abs as a bundled monoid with zero hom.