mathlib documentation

data.int.absolute_value

Absolute values and the integers #

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

Main results #

@[simp]
theorem absolute_value.map_units_int {S : Type u_2} [linear_ordered_comm_ring S] (abv : absolute_value S) (x : units ) :
abv x = 1
@[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 : units ) :
abv x = 1
@[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 : units ) (y : R) :
abv (x y) = abv y