Theorem Valuation.inversion_estimate

Modification history

2026-09-25 16:01
Mathlib/Topology/Algebra/ValuativeRel/Completion.lean
feat(Valued/ValuationTopology): creating instances of `IsValuativeTopology` on completion (#36769) …
Modified Valuation.inversion_estimateView on Github →
2023-06-01 15:15
Mathlib/Topology/Algebra/ValuedField.lean
feat: port Topology.Algebra.ValuedField (#3511)
Added Valuation.inversion_estimateView on Github →