Commit 2023-06-01 15:15 7e0afc1b

View on Github →

feat: port Topology.Algebra.ValuedField (#3511)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/ValuedField.lean

added theorem Valuation.inversion_estimate

added theorem Valued.closure_coe_completion_v_lt

added theorem Valued.continuous_extension

added theorem Valued.continuous_valuation

added theorem Valued.extension_extends

added theorem Valued.valuedCompletion_apply