Commit 2025-08-10 15:01 61d24d1c

View on Github →

feat(Topology/ValuedField): range of valuation on competion is the same as base field (#27264) and other helper API to prepare for ValuativeTopology

Estimated changes

Modified Mathlib/Topology/Algebra/Valued/ValuedField.lean

added theorem Valuation.inversion_estimate'

added theorem Valued.closure_coe_completion_v_mul_v_lt

added theorem Valued.continuous_extensionValuation

added theorem Valued.exists_coe_eq_v

added theorem Valued.extensionValuation_apply_coe

added theorem Valued.extension_eq_zero_iff

added theorem Valued.valuation_isClosedMap