Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-28 09:02 30ff9350

View on Github →

feat(topology/algebra): topological fields (#8316) Including the completion of completeable topological fields. From the perfectoid spaces project.

Estimated changes

Modified src/order/filter/basic.lean

added theorem filter.comap_comm

added theorem filter.map_comm

Modified src/topology/algebra/field.lean

added theorem topological_division_ring.continuous_units_inv

added theorem topological_division_ring.units_top_group

added theorem topological_ring.induced_units.continuous_coe

added def topological_ring.topological_space_units

added theorem topological_ring.units_embedding

added theorem topological_ring.units_topology_eq

Created src/topology/algebra/uniform_field.lean

added theorem coe_inv

added theorem continuous_hat_inv

added def hat_inv

added theorem hat_inv_extends

added theorem mul_hat_inv_cancel

Modified src/topology/basic.lean

added theorem mem_closure_image

added theorem mem_closure_of_mem_closure_union

Modified src/topology/constructions.lean

added theorem prod_induced_induced