# mathlib3documentation

algebra.order.absolute_value

# Absolute values #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines a bundled type of absolute values absolute_value R S.

## Main definitions #

• absolute_value R S is the type of absolute values on R mapping to S.
• absolute_value.abs is the "standard" absolute value on S, mapping negative x to -x.
• absolute_value.to_monoid_with_zero_hom: absolute values mapping to a linear ordered field preserve 0, * and 1
• is_absolute_value: a type class stating that f : β → α satisfies the axioms of an abs val
structure absolute_value (R : Type u_1) (S : Type u_2) [semiring R]  :
Type (max u_1 u_2)

absolute_value R S is the type of absolute values on R mapping to S: the maps that preserve *, are nonnegative, positive definite and satisfy the triangle equality.

Instances for absolute_value
@[protected, instance]
def absolute_value.zero_hom_class {R : Type u_1} {S : Type u_2} [semiring R]  :
R S
Equations
@[protected, instance]
def absolute_value.mul_hom_class {R : Type u_1} {S : Type u_2} [semiring R]  :
R S
Equations
@[protected, instance]
def absolute_value.nonneg_hom_class {R : Type u_1} {S : Type u_2} [semiring R]  :
R S
Equations
@[protected, instance]
def absolute_value.subadditive_hom_class {R : Type u_1} {S : Type u_2} [semiring R]  :
S
Equations
@[simp]
theorem absolute_value.coe_mk {R : Type u_1} {S : Type u_2} [semiring R] (f : R →ₙ* S) {h₁ : (x : R), 0 f.to_fun x} {h₂ : (x : R), f.to_fun x = 0 x = 0} {h₃ : (x y : R), f.to_fun (x + y) f.to_fun x + f.to_fun y} :
{to_mul_hom := f, nonneg' := h₁, eq_zero' := h₂, add_le' := h₃} = f
@[ext]
theorem absolute_value.ext {R : Type u_1} {S : Type u_2} [semiring R] ⦃f g : S⦄ :
( (x : R), f x = g x) f = g
def absolute_value.simps.apply {R : Type u_1} {S : Type u_2} [semiring R] (f : S) :
R S
Equations
@[protected, instance]
def absolute_value.has_coe_to_fun {R : Type u_1} {S : Type u_2} [semiring R]  :
(λ (f : S), R S)

Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun directly.

Equations
@[simp]
theorem absolute_value.coe_to_mul_hom {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) :
@[protected]
theorem absolute_value.nonneg {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) (x : R) :
0 abv x
@[protected, simp]
theorem absolute_value.eq_zero {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) {x : R} :
abv x = 0 x = 0
@[protected]
theorem absolute_value.add_le {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) (x y : R) :
abv (x + y) abv x + abv y
@[protected, simp]
theorem absolute_value.map_mul {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) (x y : R) :
abv (x * y) = abv x * abv y
@[protected]
theorem absolute_value.ne_zero_iff {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) {x : R} :
abv x 0 x 0
@[protected]
theorem absolute_value.pos {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) {x : R} (hx : x 0) :
0 < abv x
@[protected, simp]
theorem absolute_value.pos_iff {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) {x : R} :
0 < abv x x 0
@[protected]
theorem absolute_value.ne_zero {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) {x : R} (hx : x 0) :
abv x 0
theorem absolute_value.map_one_of_is_regular {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) (h : is_left_regular (abv 1)) :
abv 1 = 1
@[protected, simp]
theorem absolute_value.map_zero {R : Type u_1} {S : Type u_2} [semiring R] (abv : S) :
abv 0 = 0
@[protected]
theorem absolute_value.sub_le {R : Type u_1} {S : Type u_2} [ring R] (abv : S) (a b c : R) :
abv (a - c) abv (a - b) + abv (b - c)
@[simp]
theorem absolute_value.map_sub_eq_zero_iff {R : Type u_1} {S : Type u_2} [ring R] (abv : S) (a b : R) :
abv (a - b) = 0 a = b
@[protected, simp]
theorem absolute_value.map_one {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : S) [is_domain S] [nontrivial R] :
abv 1 = 1
@[protected, instance]
Equations
def absolute_value.to_monoid_with_zero_hom {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : S) [is_domain S] [nontrivial R] :

Absolute values from a nontrivial R to a linear ordered ring preserve *, 0 and 1.

Equations
@[simp]
def absolute_value.to_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : S) [is_domain S] [nontrivial R] :
R →* S

Absolute values from a nontrivial R to a linear ordered ring preserve * and 1.

Equations
@[simp]
theorem absolute_value.coe_to_monoid_hom {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : S) [is_domain S] [nontrivial R] :
@[protected, simp]
theorem absolute_value.map_pow {R : Type u_1} {S : Type u_2} [semiring R] [ordered_ring S] (abv : S) [is_domain S] [nontrivial R] (a : R) (n : ) :
abv (a ^ n) = abv a ^ n
@[protected]
theorem absolute_value.le_sub {R : Type u_1} {S : Type u_2} [ring R] [ordered_ring S] (abv : S) (a b : R) :
abv a - abv b abv (a - b)
@[protected, simp]
theorem absolute_value.map_neg {R : Type u_1} {S : Type u_2} [ring R] (abv : S) (a : R) :
abv (-a) = abv a
@[protected]
theorem absolute_value.map_sub {R : Type u_1} {S : Type u_2} [ring R] (abv : S) (a b : R) :
abv (a - b) = abv (b - a)
@[protected, instance]
def absolute_value.mul_ring_norm_class {R : Type u_1} {S : Type u_2} [ring R] [nontrivial R] [is_domain S] :
S
Equations
@[protected]
def absolute_value.abs {S : Type u_2}  :

absolute_value.abs is abs as a bundled absolute_value.

Equations
@[simp]
theorem absolute_value.abs_apply {S : Type u_2} (ᾰ : S) :
@[simp]
theorem absolute_value.abs_to_mul_hom_apply {S : Type u_2} (ᾰ : S) :
@[protected, instance]
def absolute_value.inhabited {S : Type u_2}  :
Equations
theorem absolute_value.abs_abv_sub_le_abv_sub {R : Type u_1} {S : Type u_2} [ring R] (abv : S) (a b : R) :
|abv a - abv b| abv (a - b)
@[class]
structure is_absolute_value {S : Type u_1} {R : Type u_2} [semiring R] (f : R S) :
Prop
• abv_nonneg : (x : R), 0 f x
• abv_eq_zero : {x : R}, f x = 0 x = 0
• abv_add : (x y : R), f (x + y) f x + f y
• abv_mul : (x y : R), f (x * y) = f x * f y

A function f is an absolute value if it is nonnegative, zero only at 0, additive, and multiplicative.

See also the type absolute_value which represents a bundled version of absolute values.

Instances of this typeclass
@[protected, instance]
def absolute_value.is_absolute_value {S : Type u_1} {R : Type u_2} [semiring R] (abv : S) :

A bundled absolute value is an absolute value.

def is_absolute_value.to_absolute_value {S : Type u_1} {R : Type u_2} [semiring R] (abv : R S) [is_absolute_value abv] :

Convert an unbundled is_absolute_value to a bundled absolute_value.

Equations
@[simp]
theorem is_absolute_value.to_absolute_value_to_mul_hom_apply {S : Type u_1} {R : Type u_2} [semiring R] (abv : R S) [is_absolute_value abv] (ᾰ : R) :
= abv ᾰ
@[simp]
theorem is_absolute_value.to_absolute_value_apply {S : Type u_1} {R : Type u_2} [semiring R] (abv : R S) [is_absolute_value abv] (ᾰ : R) :
= abv ᾰ
theorem is_absolute_value.abv_zero {S : Type u_1} {R : Type u_2} [semiring R] (abv : R S) [is_absolute_value abv] :
abv 0 = 0
theorem is_absolute_value.abv_pos {S : Type u_1} {R : Type u_2} [semiring R] (abv : R S) [is_absolute_value abv] {a : R} :
0 < abv a a 0
@[protected, instance]
theorem is_absolute_value.abv_one {S : Type u_1} [ordered_ring S] {R : Type u_2} [semiring R] (abv : R S) [is_absolute_value abv] [is_domain S] [nontrivial R] :
abv 1 = 1
def is_absolute_value.abv_hom {S : Type u_1} [ordered_ring S] {R : Type u_2} [semiring R] (abv : R S) [is_absolute_value abv] [is_domain S] [nontrivial R] :

abv as a monoid_with_zero_hom.

Equations
theorem is_absolute_value.abv_pow {S : Type u_1} [ordered_ring S] {R : Type u_2} [semiring R] [is_domain S] [nontrivial R] (abv : R S) [is_absolute_value abv] (a : R) (n : ) :
abv (a ^ n) = abv a ^ n
theorem is_absolute_value.abv_sub_le {S : Type u_1} [ordered_ring S] {R : Type u_2} [ring R] (abv : R S) [is_absolute_value abv] (a b c : R) :
abv (a - c) abv (a - b) + abv (b - c)
theorem is_absolute_value.sub_abv_le_abv_sub {S : Type u_1} [ordered_ring S] {R : Type u_2} [ring R] (abv : R S) [is_absolute_value abv] (a b : R) :
abv a - abv b abv (a - b)
theorem is_absolute_value.abv_neg {S : Type u_1} {R : Type u_2} [ring R] (abv : R S) [is_absolute_value abv] (a : R) :
abv (-a) = abv a
theorem is_absolute_value.abv_sub {S : Type u_1} {R : Type u_2} [ring R] (abv : R S) [is_absolute_value abv] (a b : R) :
abv (a - b) = abv (b - a)
theorem is_absolute_value.abs_abv_sub_le_abv_sub {S : Type u_1} {R : Type u_2} [ring R] (abv : R S) [is_absolute_value abv] (a b : R) :
|abv a - abv b| abv (a - b)
theorem is_absolute_value.abv_one' {S : Type u_1} {R : Type u_2} [semiring R] [nontrivial R] (abv : R S) [is_absolute_value abv] :
abv 1 = 1
def is_absolute_value.abv_hom' {S : Type u_1} {R : Type u_2} [semiring R] [nontrivial R] (abv : R S) [is_absolute_value abv] :

An absolute value as a monoid with zero homomorphism, assuming the target is a semifield.

Equations
theorem is_absolute_value.abv_inv {S : Type u_1} {R : Type u_2} (abv : R S) [is_absolute_value abv] (a : R) :
abv a⁻¹ = (abv a)⁻¹
theorem is_absolute_value.abv_div {S : Type u_1} {R : Type u_2} (abv : R S) [is_absolute_value abv] (a b : R) :
abv (a / b) = abv a / abv b