Theorems · Theorem · field theory

AbsoluteValue.isEquiv_of_lt_one_imp

∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : Semifield S] [inst_2 : LinearOrder S]
  {v w : AbsoluteValue R S} [IsStrictOrderedRing S] [Archimedean S] [ExistsAddOfLE S],
  v.IsNontrivial → (∀ (x : R), v x < 1 → w x < 1) → v.IsEquiv w

Defined in

Mathlib.Analysis.AbsoluteValue.Equivalence

Cited by

1 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldSemifieldLinearOrderIsStrictOrderedRingArchimedeanExistsAddOfLE