Commit 2021-10-04 08:10 edb22fef

View on Github →

feat(topology/algebra): nonarchimedean filter bases (#9511) This is preparatory material for adic topology. It is a modernized version of code from the perfectoid spaces project.

Estimated changes

Created src/topology/algebra/nonarchimedean/bases.lean

added def ring_filter_basis.module_filter_basis

added structure ring_filter_basis.submodules_basis

added theorem ring_filter_basis.submodules_basis_is_basis

added theorem ring_subgroups_basis.has_basis_nhds

added theorem ring_subgroups_basis.has_basis_nhds_zero

added theorem ring_subgroups_basis.mem_add_group_filter_basis

added theorem ring_subgroups_basis.mem_add_group_filter_basis_iff

added theorem ring_subgroups_basis.nonarchimedean

added theorem ring_subgroups_basis.of_comm

added def ring_subgroups_basis.open_add_subgroup

added def ring_subgroups_basis.to_ring_filter_basis

added def ring_subgroups_basis.topology

added structure ring_subgroups_basis

added theorem submodules_basis.nonarchimedean

added def submodules_basis.open_add_subgroup

added def submodules_basis.to_module_filter_basis

added def submodules_basis.topology

added structure submodules_basis

added theorem submodules_ring_basis.to_ring_subgroups_basis

added theorem submodules_ring_basis.to_submodules_basis

added def submodules_ring_basis.topology

added structure submodules_ring_basis