Theorems · Theorem · field theory

Valued.toNormedField.norm_le_iff

∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] {x x' : L}, ‖x‖ ≤ ‖x'‖ ↔ Valued.v x ≤ Valued.v x'

Defined in

Mathlib.Topology.Algebra.Valued.NormedValued

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderedCommGroupWithZeroValuedValuation.RankOne