Equivalence of real-valued absolute values

Two absolute values v₁, v₂ : AbsoluteValue R ℝ are equivalent if there exists a positive real number c such that v₁ x ^ c = v₂ x for all x : R.

def AbsoluteValue.IsEquiv {R : Type u_1} [Semiring R] (f g : AbsoluteValue R ℝ) : Prop

Two absolute values f, g on R with values in ℝ are equivalent if there exists a positive real constant c such that for all x : R, (f x)^c = g x.

Equations

• f.IsEquiv g = ∃ (c : ℝ), 0 < c ∧ (fun (x : R) => f x ^ c) = ⇑g

theorem AbsoluteValue.isEquiv_refl {R : Type u_1} [Semiring R] (f : AbsoluteValue R ℝ) : f.IsEquiv f

Equivalence of absolute values is reflexive.

theorem AbsoluteValue.isEquiv_symm {R : Type u_1} [Semiring R] {f g : AbsoluteValue R ℝ} (hfg : f.IsEquiv g) : g.IsEquiv f

Equivalence of absolute values is symmetric.

theorem AbsoluteValue.isEquiv_trans {R : Type u_1} [Semiring R] {f g k : AbsoluteValue R ℝ} (hfg : f.IsEquiv g) (hgk : g.IsEquiv k) : f.IsEquiv k

Equivalence of absolute values is transitive.

instance AbsoluteValue.instSetoidReal {R : Type u_1} [Semiring R] : Setoid (AbsoluteValue R ℝ)

Equations

• AbsoluteValue.instSetoidReal = { r := AbsoluteValue.IsEquiv, iseqv := ⋯ }

@[simp]

theorem AbsoluteValue.eq_trivial_of_isEquiv_trivial {R : Type u_1} [Semiring R] [DecidablePred fun (x : R) => x = 0] [NoZeroDivisors R] (f : AbsoluteValue R ℝ) : f ≈ AbsoluteValue.trivial ↔ f = AbsoluteValue.trivial

An absolute value is equivalent to the trivial iff it is trivial itself.