Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-05 08:05 c42786f5

View on Github →

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

Estimated changes

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

added theorem ideal.adic_basis

added theorem ideal.adic_module_basis

added def ideal.adic_module_topology

added def ideal.adic_topology

added theorem ideal.has_basis_nhds_adic

added theorem ideal.has_basis_nhds_zero_adic

added theorem ideal.nonarchimedean

added def ideal.open_add_subgroup

added def ideal.ring_filter_basis

added def is_adic

added theorem is_adic_iff

added theorem is_bot_adic_iff

added theorem is_ideal_adic_pow

added def with_ideal.topological_space_module