Commit 2022-06-01 09:59 7d713439

View on Github →

chore(topology/algebra/uniform_field): Wrap in namespace (#14498) Put everything in topology.algebra.uniform_field in the uniform_space.completion namespace.

Estimated changes

Modified src/number_theory/function_field.lean

Modified src/ring_theory/dedekind_domain/adic_valuation.lean

Modified src/topology/algebra/uniform_field.lean

deleted theorem coe_inv

deleted theorem continuous_hat_inv

deleted def hat_inv

deleted theorem hat_inv_extends

deleted theorem mul_hat_inv_cancel

added theorem uniform_space.completion.coe_inv

added theorem uniform_space.completion.continuous_hat_inv

added def uniform_space.completion.hat_inv

added theorem uniform_space.completion.hat_inv_extends

added theorem uniform_space.completion.mul_hat_inv_cancel