mathlib3 documentation

algebra.abs

Absolute value #

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

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

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