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

ink

@[simp]

theorem AbsoluteValue.map_units_int {S : Type u_1} [inst : LinearOrderedCommRing S] (abv : AbsoluteValue ℤ S) (x : ℤˣ) : ↑abv ↑x = 1

ink

@[simp]

theorem AbsoluteValue.map_units_int_cast {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst : LinearOrderedCommRing S] [inst : Nontrivial R] (abv : AbsoluteValue R S) (x : ℤˣ) : ↑abv ↑↑x = 1

ink

@[simp]

theorem AbsoluteValue.map_units_int_smul {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst : LinearOrderedCommRing S] (abv : AbsoluteValue R S) (x : ℤˣ) (y : R) : ↑abv (x • y) = ↑abv y

ink

@[simp]

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

ink

def Int.natAbsHom : ℤ →*₀ ℕ

Int.natAbs as a bundled monoid with zero hom.

Equations

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