mathlib3 documentation

data.int.absolute_value

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 #

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