Documentation

Mathlib.Data.Int.AbsoluteValue

Absolute values and the integers #

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

Main results #

@[simp]
theorem AbsoluteValue.map_units_int {S : Type u_2} [LinearOrderedCommRing S] (abv : AbsoluteValue S) (x : ˣ) :
abv x = 1
@[simp]
theorem AbsoluteValue.map_units_intCast {R : Type u_1} {S : Type u_2} [Ring R] [LinearOrderedCommRing S] [Nontrivial R] (abv : AbsoluteValue R S) (x : ˣ) :
abv x = 1
@[deprecated AbsoluteValue.map_units_intCast]
theorem AbsoluteValue.map_units_int_cast {R : Type u_1} {S : Type u_2} [Ring R] [LinearOrderedCommRing S] [Nontrivial R] (abv : AbsoluteValue R S) (x : ˣ) :
abv x = 1

Alias of AbsoluteValue.map_units_intCast.

@[simp]
theorem AbsoluteValue.map_units_int_smul {R : Type u_1} {S : Type u_2} [Ring R] [LinearOrderedCommRing S] (abv : AbsoluteValue R S) (x : ˣ) (y : R) :
abv (x y) = abv y
@[simp]
theorem Int.natAbsHom_apply (m : ) :
Int.natAbsHom m = m.natAbs

Int.natAbs as a bundled monoid with zero hom.

Equations
Instances For