Documentation

Mathlib.Topology.Algebra.Valued.NormedValued

Correspondence between nontrivial nonarchimedean norms and rank one valuations #

Nontrivial nonarchimedean norms correspond to rank one valuations.

Main Definitions #

Tags #

norm, nonarchimedean, nontrivial, valuation, rank one

The valuation on a nonarchimedean normed field K defined as nnnorm.

Equations
  • NormedField.valuation h = { toFun := nnnorm, map_zero' := , map_one' := , map_mul' := , map_add_le_max' := h }
Instances For
    def NormedField.toValued {K : Type u_1} [hK : NormedField K] (h : IsNonarchimedean norm) :

    The valued field structure on a nonarchimedean normed field K, determined by the norm.

    Equations
    Instances For
      def Valued.norm {L : Type u_2} [Field L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] :
      L

      The norm function determined by a rank one valuation on a field L.

      Equations
      Instances For
        theorem Valued.norm_nonneg {L : Type u_2} [Field L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] (x : L) :
        theorem Valued.norm_add_le {L : Type u_2} [Field L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] (x : L) (y : L) :
        theorem Valued.norm_eq_zero {L : Type u_2} [Field L] {Γ₀ : Type u_3} [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] {x : L} (hx : Valued.norm x = 0) :
        x = 0
        def Valued.toNormedField (L : Type u_2) [Field L] (Γ₀ : Type u_3) [LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀] [hv : Valued.v.RankOne] :

        The normed field structure determined by a rank one valuation.

        Equations
        Instances For