Mathlib Map

Theorems · Definition · field theory

Valued.toNontriviallyNormedField

(L : Type u_1) →
  [inst : Field L] →
    (Γ₀ : Type u_2) →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        [val : Valued L Γ₀] → [hv : Valued.v.RankOne] → NontriviallyNormedField L

The nontrivially normed field structure determined by a rank one valuation.

Defined in
Mathlib.Topology.Algebra.Valued.NormedValued
Cited by
0 results in Mathlib
Foundations
Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FieldLinearOrderedCommGroupWithZeroValuedValuation.RankOne
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

NontriviallyNormedField · cited by 8742NontriviallyNormedFieldField · cited by 7404FieldNormedField · cited by 1084NormedFieldLinearOrderedCommGroupWithZero · cited by 528LinearOrderedCommGroupWit…Valued.v · cited by 163Valued.vValued · cited by 70ValuedValuation.RankOne · cited by 32Valuation.RankOneValued.toNormedField · cited by 13Valued.toNormedFieldValued.toNontriviallyNormedFi…CITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.