Theorem Valuation.inversion_estimate'

Modification history

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 →