Theorems · Inductive type · order theory

IsAbsoluteValue

{S : Type u_5} → [Semiring S] → [PartialOrder S] → {R : Type u_6} → [Semiring R] → (R → S) → Prop

A function f is an absolute value if it is nonnegative, zero only at 0, additive, and multiplicative. See also the type AbsoluteValue which represents a bundled version of absolute values.

Defined in

Mathlib.Algebra.Order.AbsoluteValue.Basic

Cited by

160 results in Mathlib

Foundations

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

Assumes

SemiringPartialOrderSemiring