Theorems · Definition · field theory

Valued.toNormedField

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

The normed field structure determined by a rank one valuation.

Defined in: Mathlib.Topology.Algebra.Valued.NormedValued
Cited by: 13 results in Mathlib
Foundations: Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field LinearOrderedCommGroupWithZero Valued Valuation.RankOne

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites6

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

Fieldstatement and proof · cited by 7,404
NormedFieldstatement · cited by 1,084
LinearOrderedCommGroupWithZerostatement and proof · cited by 528
Valued.vstatement and proof · cited by 163
Valuedstatement and proof · cited by 70
Valuation.RankOnestatement and proof · cited by 32

Cited by14

Results whose statement or proof uses this declaration.

Valued.toNormedField.setOfPred_mem_integer_eq_closedBallstatement · cited by 3
Valued.toNormedField.norm_lt_one_iffstatement · cited by 1
Valued.toNormedField.norm_defstatement · cited by 0
Valued.toNormedField.norm_le_iffstatement · cited by 0
Valued.toNormedField.norm_le_one_iffstatement · cited by 0
Valued.toNormedField.norm_lt_iffstatement · cited by 0
Valued.toNormedField.one_le_norm_iffstatement · cited by 0
Valued.integer.properSpace_iff_compactSpace_integerstatement · cited by 0
Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueFieldstatement · cited by 0
Valued.toNormedField.one_lt_norm_iffstatement · cited by 0
Valued.toNormedField.setOf_mem_integer_eq_closedBallstatement · cited by 0
Valued.toNontriviallyNormedFieldproof · cited by 0