Theorems · Theorem · field theory
Valued.toNormedField.norm_lt_one_iff
∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
[hv : Valued.v.RankOne] {x : L}, ‖x‖ < 1 ↔ Valued.v x < 1- Cited by
- 1 results in Mathlib
- Foundations
- Depth 119 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Realstatement · cited by 25,697
- Fieldstatement and proof · cited by 7,404
- Norm.normstatement and proof · cited by 5,413
- map_oneproof · cited by 861
- Valuationstatement · cited by 823
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
- Valued.vstatement and proof · cited by 163
- Valuation.restrictproof · cited by 112
- StrictMono.lt_iff_ltproof · cited by 86
- Valuedstatement and proof · cited by 70
- Valuation.RankOnestatement and proof · cited by 32
Cited by1
Results whose statement or proof uses this declaration.
- Valued.integer.totallyBounded_iff_finite_residueFieldproof · cited by 1