Theorems · Theorem · field theory
AbsoluteValue.isEquiv_iff_exists_rpow_eq
∀ {F : Type u_1} [inst : Field F] {v w : AbsoluteValue F ℝ}, v.IsEquiv w ↔ ∃ c, 0 < c ∧ (fun x => v x ^ c) = ⇑wIf v and w are two real absolute values on a field F, then v and w are equivalent if
and only if there exists a positive real constant c such that for all x : R, (f x)^c = g x.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 200 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites32
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
- Realstatement and proof · cited by 25,697
- Fieldstatement and proof · cited by 7,404
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- eq_or_neproof · cited by 1,117
- Real.logproof · cited by 939
- zero_lt_oneproof · cited by 598
- Iff.notproof · cited by 489
- AbsoluteValuestatement and proof · cited by 363
- sub_eq_zero_of_eqproof · cited by 154
- div_eq_inv_mulproof · cited by 146
Cited by4
Results whose statement or proof uses this declaration.
- Rat.AbsoluteValue.exists_nat_rpow_iff_isEquivproof · cited by 1
- NumberField.InfinitePlace.eq_iff_isEquivproof · cited by 1
- AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zeroproof · cited by 1
- Rat.AbsoluteValue.not_real_isEquiv_padicproof · cited by 0