Theorems · Definition · field theory

AbsoluteValue.IsEquiv

{R : Type u_1} →
  [inst : Semiring R] →
    {S : Type u_2} → [inst_1 : Semiring S] → [inst_2 : PartialOrder S] → AbsoluteValue R S → AbsoluteValue R S → Prop

Two absolute values v and w are equivalent if v x ≤ v y precisely when w x ≤ w y. Note that for real absolute values this condition is equivalent to the existence of a positive real number c such that v x ^ c = w x for all x. See AbsoluteValue.isEquiv_iff_exists_rpow_eq.

Defined in

Mathlib.Analysis.AbsoluteValue.Equivalence

Cited by

32 results in Mathlib

Foundations

Depth 17 from the axioms · uses no axioms

Assumes

SemiringSemiringPartialOrder