Theorems · Theorem · field theory
Valuation.inversion_estimate
∀ {K : Type u_1} [inst : DivisionRing K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
(v : Valuation K Γ₀) {x y : K} {γ : Γ₀ˣ}, y ≠ 0 → v (x - y) < min (↑γ * (v y * v y)) (v y) → v (x⁻¹ - y⁻¹) < ↑γ- Cited by
- 1 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
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
- mul_oneproof · cited by 3,885
- one_mulproof · cited by 2,841
- Unitsstatement and proof · cited by 2,804
- mul_commproof · cited by 2,262
- Units.valstatement and proof · cited by 1,966
- mul_assocproof · cited by 1,667
- DivisionRingstatement and proof · cited by 1,062
- Valuationstatement and proof · cited by 823
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
- lt_of_lt_of_leproof · cited by 438
- mul_inv_revproof · cited by 270
Cited by1
Results whose statement or proof uses this declaration.
- Valuation.inversion_estimate'proof · cited by 0