Theorems · Inductive type · order theory

AbsoluteValue

(R : Type u_5) → (S : Type u_6) → [Semiring R] → [Semiring S] → [PartialOrder S] → Type (max u_5 u_6)

AbsoluteValue R S is the type of absolute values on R mapping to S: the maps that preserve *, are nonnegative, positive definite and satisfy the triangle inequality.

Defined in

Mathlib.Algebra.Order.AbsoluteValue.Basic

Cited by

363 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

SemiringSemiringPartialOrder