algebra.abs

# Absolute value #

This file defines a notational class has_abs which adds the unary operator abs and the notation |.|. The concept of an absolute value occurs in lattice ordered groups and in GL and GM spaces.

Mathematical structures possessing an absolute value often also possess a unique decomposition of elements into "positive" and "negative" parts which are in some sense "disjoint" (e.g. the Jordan decomposition of a measure). This file also defines has_pos_part and has_neg_part classes which add unary operators pos and neg, representing the maps taking an element to its positive and negative part respectively along with the notation ⁺ and ⁻.

## Notations #

The following notation is introduced:

• |.| for the absolute value;
• .⁺ for the positive part;
• .⁻ for the negative part.

## Tags #

absolute

@[class]
structure has_abs (α : Type u_1) :
Type u_1
• abs : α → α

Absolute value is a unary operator with properties similar to the absolute value of a real number.

Instances of this typeclass
Instances of other typeclasses for has_abs
• has_abs.has_sizeof_inst
@[class]
structure has_pos_part (α : Type u_1) :
Type u_1
• pos : α → α

The positive part of an element admiting a decomposition into positive and negative parts.

Instances of this typeclass
Instances of other typeclasses for has_pos_part
• has_pos_part.has_sizeof_inst
@[class]
structure has_neg_part (α : Type u_1) :
Type u_1
• neg : α → α

The negative part of an element admiting a decomposition into positive and negative parts.

Instances of this typeclass
Instances of other typeclasses for has_neg_part
• has_neg_part.has_sizeof_inst