# 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
• abs : αα

The absolute value function.

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
• pos : αα

The positive part function.

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

Instances
class NegPart (α : Type u_1) :
Type u_1
• neg : αα

The negative part function.

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

Instances

The absolute value function.

Instances For

Unexpander for the notation |a| for abs a. Tries to add discretionary parentheses in unparseable cases.

Instances For

The positive part function.

Instances For

The negative part function.

Instances For