# Documentation

Mathlib.Algebra.Abs

# Absolute value #

This file defines a notational class 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 PosPart and NegPart 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 Abs (α : Type u_1) :
Type u_1
• The absolute value function.

abs : αα

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

Instances
class PosPart (α : Type u_1) :
Type u_1
• The positive part function.

pos : αα

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

Instances
class NegPart (α : Type u_1) :
Type u_1
• The negative part function.

neg : αα

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

Instances

The absolute value function.

Equations
• One or more equations did not get rendered due to their size.

The positive part function.

Equations

The negative part function.

Equations