mathlib documentation

data.int.absolute_value

Absolute values and the integers #

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

Main results #

source
@[simp]
theorem absolute_value.map_units_int {S : Type u_2} [linear_ordered_comm_ring S] (abv : absolute_value ℤ S) (x : ℤˣ) :
⇑abv ↑x = 1
source
@[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 : ℤˣ) :
⇑abv ↑↑x = 1
source
@[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) :
⇑abv (x • y) = ⇑abv y