Theorems · Theorem · field theory
Valued.toNormedField.one_lt_norm_iff
∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
[hv : Valued.v.RankOne] {x : L}, 1 < ‖x‖ ↔ 1 < Valued.v x- Cited by
- 0 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 by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.