Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-07 21:23 9518ce12

View on Github →

feat(topology/algebra): valued fields (#9589) This is a modernized version of code from the perfectoid spaces project.

Estimated changes

Modified src/algebra/group_with_zero/basic.lean

added theorem group_with_zero.eq_zero_or_unit

Modified src/ring_theory/valuation/basic.lean

added def valuation.lt_add_subgroup

Modified src/topology/algebra/uniform_group.lean

added theorem topological_add_group.separated_iff_zero_closed

added theorem topological_add_group.separated_of_zero_sep

Created src/topology/algebra/valuation.lean

added theorem valued.cauchy_iff

added theorem valued.loc_const

added theorem valued.mem_nhds

added theorem valued.mem_nhds_zero

added theorem valued.subgroups_basis

Created src/topology/algebra/valued_field.lean

added theorem valuation.inversion_estimate

added theorem valued.continuous_extension

added theorem valued.continuous_valuation

added theorem valued.extension_extends

Modified src/topology/basic.lean

added theorem dense_range.mem_nhds