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_estimate'View on Github →

2025-08-10 15:01

Mathlib/Topology/Algebra/Valued/ValuedField.lean

feat(Topology/ValuedField): range of valuation on competion is the same as base field (#27264) …

Added Valuation.inversion_estimate'View on Github →