Absolute values and the integers

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

Main results

• AbsoluteValue.map_units_int: an absolute value sends all units of ℤ to 1
• Int.natAbsHom: Int.natAbs bundled as a MonoidWithZeroHom

@[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

def Int.natAbsHom : ℤ →*₀ ℕ

Int.natAbs as a bundled monoid with zero hom.

Equations

• Int.natAbsHom = { toFun := Int.natAbs, map_zero' := Int.natAbs_zero, map_one' := Int.natAbs_one, map_mul' := Int.natAbs_mul }

@[simp]

theorem Int.natAbsHom_apply (m : ℤ) : Int.natAbsHom m = m.natAbs