Theorems · Theorem · field theory
AbsoluteValue.isEquiv_iff_lt_one_iff
∀ {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], v.IsEquiv w ↔ ∀ (x : R), v x < 1 ↔ w x < 1- Cited by
- 3 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- LinearOrderstatement and proof · cited by 8,572
- Fieldstatement and proof · cited by 7,404
- one_mulproof · cited by 2,841
- IsStrictOrderedRingstatement and proof · cited by 2,490
- map_mulproof · cited by 1,137
- eq_or_neproof · cited by 1,117
- Semifieldstatement and proof · cited by 439
- AbsoluteValuestatement and proof · cited by 363
- map_inv₀proof · cited by 106
- AbsoluteValue.IsEquivstatement and proof · cited by 32
- le_iff_le_iff_lt_iff_ltproof · cited by 25
Cited by3
Results whose statement or proof uses this declaration.
- AbsoluteValue.isEquiv_iff_exists_rpow_eqproof · cited by 4
- AbsoluteValue.isEquiv_of_lt_one_impproof · cited by 1
- AbsoluteValue.isEquiv_iff_isHomeomorphproof · cited by 0