Theorems · Definition · order theory

IsAbsoluteValue.toAbsoluteValue

{S : Type u_5} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      {R : Type u_6} → [inst_2 : Semiring R] → (abv : R → S) → [IsAbsoluteValue abv] → AbsoluteValue R S

Convert an unbundled IsAbsoluteValue to a bundled AbsoluteValue.

Defined in

Mathlib.Algebra.Order.AbsoluteValue.Basic

Cited by

12 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SemiringPartialOrderSemiringIsAbsoluteValue