mathlib documentation

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:

Tags #

absolute

source
@[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
source
@[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.

source
@[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.