Theorems · Definition · field theory
NormedField.toValued
{K : Type u_1} → [hK : NormedField K] → [IsUltrametricDist K] → Valued K NNRealThe valued field structure on a nonarchimedean normed field K, determined by the norm.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 163 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- NormedFieldIsUltrametricDist
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- NNRealstatement · cited by 4,310
- UniformSpaceproof · cited by 2,040
- NormedFieldstatement and proof · cited by 1,084
- IsUniformAddGroupproof · cited by 342
- IsUltrametricDiststatement and proof · cited by 177
- Valuedstatement · cited by 70
- NormedField.valuationproof · cited by 6
Cited by14
Results whose statement or proof uses this declaration.
- Valued.integer.exists_norm_coe_lt_onestatement · cited by 2
- Valued.integer.mem_iffstatement · cited by 1
- Valued.integer.norm_coe_unitstatement · cited by 1
- Valued.integer.exists_norm_lt_onestatement · cited by 0
- Irreducible.maximalIdeal_eq_closedBallstatement · cited by 0
- Valued.integer.isUnit_iff_norm_eq_onestatement · cited by 0
- Irreducible.maximalIdeal_pow_eq_closedBall_powstatement · cited by 0
- Valued.integer.norm_irreducible_lt_onestatement · cited by 0
- Valued.integer.norm_irreducible_posstatement · cited by 0
- Valued.integer.norm_le_onestatement · cited by 0
- Valued.integer.norm_unitstatement · cited by 0
- Valued.integer.coe_span_singleton_eq_closedBallstatement · cited by 0